THEOREM
*******
Elementary propositions in group theory:
1. Right cancellation of * Line 9
2. Left cancellation of * Line 54
3. Determine identity (right) Line 210
4. Determine identity (left) Line 238
5. Determine inverse (right & left) Line 135
6. inv(e)=e Line 199
7. inv(inv(x)) = x Line 95
8. inv(x*y) = inv(y)*inv(x) Line 265
This fomral proof was written and machine-verified with the aid of the author's DC Proof 2.0 available at http://www.dcproof.com
Suppose (g,*) is group with identity e and inverse operator inv
1 Set(g)
& ALL(a):ALL(b):[a e g & b e g => a*b e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
Premise
Define: g
2 Set(g)
Split, 1
Define: *
3 ALL(a):ALL(b):[a e g & b e g => a*b e g]9
Split, 1
4 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
Split, 1
Define: e
5 e e g
Split, 1
6 ALL(a):[a e g => a*e=a & e*a=a]
Split, 1
Define: inv
7 ALL(a):[a e g => inv(a) e g]
Split, 1
8 ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
Split, 1
Right cancellation
******************
Prove: ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
Suppose...
9 x e g & y e g & z e g
Premise
10 x e g
Split, 9
11 y e g
Split, 9
12 z e g
Split, 9
Prove: x*y=z*y => x=z
Suppose...
13 x*y=z*y
Premise
14 x*y*inv(y)=x*y*inv(y)
Reflex
15 x*y*inv(y)=z*y*inv(y)
Substitute, 13, 14
Apply associativity
16 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 4
17 ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]
U Spec, 16
18 x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))
U Spec, 17
19 y e g => inv(y) e g
U Spec, 7
20 inv(y) e g
Detach, 19, 11
21 x e g & y e g
Join, 10, 11
22 x e g & y e g & inv(y) e g
Join, 21, 20
23 x*y*inv(y)=x*(y*inv(y))
Detach, 18, 22
24 x*(y*inv(y))=z*y*inv(y)
Substitute, 23, 15
Apply definition of inv
25 y e g => y*inv(y)=e & inv(y)*y=e
U Spec, 8
26 y*inv(y)=e & inv(y)*y=e
Detach, 25, 11
27 y*inv(y)=e
Split, 26
28 inv(y)*y=e
Split, 26
29 x*e=z*y*inv(y)
Substitute, 27, 24
30 x e g => x*e=x & e*x=x
U Spec, 6
31 x*e=x & e*x=x
Detach, 30, 10
32 x*e=x
Split, 31
33 e*x=x
Split, 31
34 x=z*y*inv(y)
Substitute, 32, 29
Apply associativity
35 ALL(b):ALL(c):[z e g & b e g & c e g => z*b*c=z*(b*c)]
U Spec, 4
36 ALL(c):[z e g & y e g & c e g => z*y*c=z*(y*c)]
U Spec, 35
37 z e g & y e g & inv(y) e g => z*y*inv(y)=z*(y*inv(y))
U Spec, 36
38 z e g & y e g
Join, 12, 11
39 z e g & y e g & inv(y) e g
Join, 38, 20
40 z*y*inv(y)=z*(y*inv(y))
Detach, 37, 39
41 x=z*(y*inv(y))
Substitute, 40, 34
42 y e g => y*inv(y)=e & inv(y)*y=e
U Spec, 8
43 y*inv(y)=e & inv(y)*y=e
Detach, 42, 11
44 y*inv(y)=e
Split, 43
45 inv(y)*y=e
Split, 43
46 x=z*e
Substitute, 44, 41
47 z e g => z*e=z & e*z=z
U Spec, 6
48 z*e=z & e*z=z
Detach, 47, 12
49 z*e=z
Split, 48
50 e*z=z
Split, 48
51 x=z
Substitute, 49, 46
As Required:
52 x*y=z*y => x=z
4 Conclusion, 13
As Required:
53 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
4 Conclusion, 9
Left cancellation
*****************
Prove: ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
Suppose...
54 x e g & y e g & z e g
Premise
55 x e g
Split, 54
56 y e g
Split, 54
57 z e g
Split, 54
Prove: x*y=x*z => y=z
Suppose...
58 x*y=x*z
Premise
59 inv(x)*(x*y)=inv(x)*(x*y)
Reflex
60 inv(x)*(x*y)=inv(x)*(x*z)
Substitute, 58, 59
Apply associativity
61 ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]
U Spec, 4
62 ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]
U Spec, 61
63 inv(x) e g & x e g & y e g => inv(x)*x*y=inv(x)*(x*y)
U Spec, 62
64 x e g => inv(x) e g
U Spec, 7
65 inv(x) e g
Detach, 64, 55
66 inv(x) e g & x e g
Join, 65, 55
67 inv(x) e g & x e g & y e g
Join, 66, 56
68 inv(x)*x*y=inv(x)*(x*y)
Detach, 63, 67
69 inv(x)*x*y=inv(x)*(x*z)
Substitute, 68, 60
70 x e g => x*inv(x)=e & inv(x)*x=e
U Spec, 8
71 x*inv(x)=e & inv(x)*x=e
Detach, 70, 55
72 x*inv(x)=e
Split, 71
73 inv(x)*x=e
Split, 71
74 e*y=inv(x)*(x*z)
Substitute, 73, 69
75 y e g => y*e=y & e*y=y
U Spec, 6
76 y*e=y & e*y=y
Detach, 75, 56
77 y*e=y
Split, 76
78 e*y=y
Split, 76
79 y=inv(x)*(x*z)
Substitute, 78, 74
Apply associativity
80 ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]
U Spec, 4
81 ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]
U Spec, 80
82 inv(x) e g & x e g & z e g => inv(x)*x*z=inv(x)*(x*z)
U Spec, 81
83 inv(x) e g & x e g
Join, 65, 55
84 inv(x) e g & x e g & z e g
Join, 83, 57
85 inv(x)*x*z=inv(x)*(x*z)
Detach, 82, 84
86 y=inv(x)*x*z
Substitute, 85, 79
87 y=e*z
Substitute, 73, 86
88 z e g => z*e=z & e*z=z
U Spec, 6
89 z*e=z & e*z=z
Detach, 88, 57
90 z*e=z
Split, 89
91 e*z=z
Split, 89
92 y=z
Substitute, 91, 87
93 x*y=x*z => y=z
4 Conclusion, 58
As Required:
94 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
4 Conclusion, 54
inv(inv(x))=x
*************
Prove: ALL(a):[a e g => inv(inv(a))=a]
Suppose...
95 x e g
Premise
Apply definition of inv
96 x e g => x*inv(x)=e & inv(x)*x=e
U Spec, 8
97 x*inv(x)=e & inv(x)*x=e
Detach, 96, 95
98 x*inv(x)=e
Split, 97
99 inv(x)*x=e
Split, 97
Apply definition of inv
100 inv(x) e g => inv(x)*inv(inv(x))=e & inv(inv(x))*inv(x)=e
U Spec, 8
101 x e g => inv(x) e g
U Spec, 7
102 inv(x) e g
Detach, 101, 95
103 inv(x)*inv(inv(x))=e & inv(inv(x))*inv(x)=e
Detach, 100, 102
104 inv(x)*inv(inv(x))=e
Split, 103
105 inv(inv(x))*inv(x)=e
Split, 103
106 e*x=e*x
Reflex
107 inv(inv(x))*inv(x)*x=e*x
Substitute, 105, 106
Apply associativity
108 ALL(b):ALL(c):[inv(inv(x)) e g & b e g & c e g => inv(inv(x))*b*c=inv(inv(x))*(b*c)]
U Spec, 4
109 ALL(c):[inv(inv(x)) e g & inv(x) e g & c e g => inv(inv(x))*inv(x)*c=inv(inv(x))*(inv(x)*c)]
U Spec, 108
110 inv(inv(x)) e g & inv(x) e g & x e g => inv(inv(x))*inv(x)*x=inv(inv(x))*(inv(x)*x)
U Spec, 109
111 inv(x) e g => inv(inv(x)) e g
U Spec, 7
112 x e g => inv(x) e g
U Spec, 7
113 inv(x) e g
Detach, 112, 95
114 inv(inv(x)) e g
Detach, 111, 113
115 inv(inv(x)) e g & inv(x) e g
Join, 114, 113
116 inv(inv(x)) e g & inv(x) e g & x e g
Join, 115, 95
117 inv(inv(x))*inv(x)*x=inv(inv(x))*(inv(x)*x)
Detach, 110, 116
118 inv(inv(x))*(inv(x)*x)=e*x
Substitute, 117, 107
Apply definition of inv
119 x e g => x*inv(x)=e & inv(x)*x=e
U Spec, 8
120 x*inv(x)=e & inv(x)*x=e
Detach, 119, 95
121 x*inv(x)=e
Split, 120
122 inv(x)*x=e
Split, 120
123 inv(inv(x))*e=e*x
Substitute, 122, 118
Apply definition of e
124 inv(inv(x)) e g => inv(inv(x))*e=inv(inv(x)) & e*inv(inv(x))=inv(inv(x))
U Spec, 6
125 inv(inv(x))*e=inv(inv(x)) & e*inv(inv(x))=inv(inv(x))
Detach, 124, 114
126 inv(inv(x))*e=inv(inv(x))
Split, 125
127 e*inv(inv(x))=inv(inv(x))
Split, 125
128 inv(inv(x))=e*x
Substitute, 126, 123
129 x e g => x*e=x & e*x=x
U Spec, 6
130 x*e=x & e*x=x
Detach, 129, 95
131 x*e=x
Split, 130
132 e*x=x
Split, 130
133 inv(inv(x))=x
Substitute, 132, 128
As Required:
134 ALL(a):[a e g => inv(inv(a))=a]
4 Conclusion, 95
Determine inverse (right & left)
********************************
Prove: ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
Suppose...
135 x e g & y e g
Premise
136 x e g
Split, 135
137 y e g
Split, 135
Prove: x*y=e => inv(x)=y & inv(y)=x
Suppose
138 x*y=e
Premise
Apply definition of inv
139 x e g => x*inv(x)=e & inv(x)*x=e
U Spec, 8
140 x*inv(x)=e & inv(x)*x=e
Detach, 139, 136
141 x*inv(x)=e
Split, 140
142 inv(x)*x=e
Split, 140
143 inv(x)*x*y=inv(x)*x*y
Reflex
144 e*y=inv(x)*x*y
Substitute, 142, 143
Apply definition of e
145 y e g => y*e=y & e*y=y
U Spec, 6
146 y*e=y & e*y=y
Detach, 145, 137
147 y*e=y
Split, 146
148 e*y=y
Split, 146
149 y=inv(x)*x*y
Substitute, 148, 144
Apply associativity
150 ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]
U Spec, 4
151 ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]
U Spec, 150
152 inv(x) e g & x e g & y e g => inv(x)*x*y=inv(x)*(x*y)
U Spec, 151
153 x e g => inv(x) e g
U Spec, 7
154 inv(x) e g
Detach, 153, 136
155 inv(x) e g & x e g
Join, 154, 136
156 inv(x) e g & x e g & y e g
Join, 155, 137
157 inv(x)*x*y=inv(x)*(x*y)
Detach, 152, 156
158 y=inv(x)*(x*y)
Substitute, 157, 149
159 y=inv(x)*e
Substitute, 138, 158
160 inv(x) e g => inv(x)*e=inv(x) & e*inv(x)=inv(x)
U Spec, 6
161 inv(x)*e=inv(x) & e*inv(x)=inv(x)
Detach, 160, 154
162 inv(x)*e=inv(x)
Split, 161
163 e*inv(x)=inv(x)
Split, 161
As Required:
164 y=inv(x)
Substitute, 162, 159
165 y e g => y*inv(y)=e & inv(y)*y=e
U Spec, 8
166 y*inv(y)=e & inv(y)*y=e
Detach, 165, 137
167 y*inv(y)=e
Split, 166
168 inv(y)*y=e
Split, 166
169 x*y*inv(y)=x*y*inv(y)
Reflex
170 e*inv(y)=x*y*inv(y)
Substitute, 138, 169
Apply definition of e
171 inv(y) e g => inv(y)*e=inv(y) & e*inv(y)=inv(y)
U Spec, 6
172 y e g => inv(y) e g
U Spec, 7
173 inv(y) e g
Detach, 172, 137
174 inv(y)*e=inv(y) & e*inv(y)=inv(y)
Detach, 171, 173
175 inv(y)*e=inv(y)
Split, 174
176 e*inv(y)=inv(y)
Split, 174
177 inv(y)=x*y*inv(y)
Substitute, 176, 170
Apply associativity
178 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 4
179 ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]
U Spec, 178
180 x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))
U Spec, 179
181 x e g & y e g
Join, 136, 137
182 x e g & y e g & inv(y) e g
Join, 181, 173
183 x*y*inv(y)=x*(y*inv(y))
Detach, 180, 182
184 inv(y)=x*(y*inv(y))
Substitute, 183, 177
185 y e g => y*inv(y)=e & inv(y)*y=e
U Spec, 8
186 y*inv(y)=e & inv(y)*y=e
Detach, 185, 137
187 y*inv(y)=e
Split, 186
188 inv(y)*y=e
Split, 186
189 inv(y)=x*e
Substitute, 187, 184
190 x e g => x*e=x & e*x=x
U Spec, 6
191 x*e=x & e*x=x
Detach, 190, 136
192 x*e=x
Split, 191
193 e*x=x
Split, 191
As Required:
194 inv(y)=x
Substitute, 192, 189
195 inv(x)=y
Sym, 164
196 inv(x)=y & inv(y)=x
Join, 195, 194
As Required:
197 x*y=e => inv(x)=y & inv(y)=x
4 Conclusion, 138
As Required:
198 ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
4 Conclusion, 135
inv(e)=e
********
Prove: inv(e)=e
Apply previous result
199 ALL(b):[e e g & b e g => [e*b=e => inv(e)=b & inv(b)=e]]
U Spec, 198
200 e e g & e e g => [e*e=e => inv(e)=e & inv(e)=e]
U Spec, 199
201 e e g & e e g
Join, 5, 5
202 e*e=e => inv(e)=e & inv(e)=e
Detach, 200, 201
203 e e g => e*e=e & e*e=e
U Spec, 6
204 e*e=e & e*e=e
Detach, 203, 5
205 e*e=e
Split, 204
206 e*e=e
Split, 204
207 inv(e)=e & inv(e)=e
Detach, 202, 206
208 inv(e)=e
Split, 207
As Required:
209 inv(e)=e
Split, 207
Determine identity (right)
**************************
Prove: ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
Suppose...
210 x e g & y e g
Premise
211 x e g
Split, 210
212 y e g
Split, 210
Prove: x*y=x => y=e
Suppose...
213 x*y=x
Premise
214 inv(x)*x=inv(x)*x
Reflex
215 inv(x)*(x*y)=inv(x)*x
Substitute, 213, 214
Apply definition of inv
216 x e g => x*inv(x)=e & inv(x)*x=e
U Spec, 8
217 x*inv(x)=e & inv(x)*x=e
Detach, 216, 211
218 x*inv(x)=e
Split, 217
219 inv(x)*x=e
Split, 217
220 inv(x)*(x*y)=e
Substitute, 219, 215
Apply associativity
221 ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]
U Spec, 4
222 ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]
U Spec, 221
223 inv(x) e g & x e g & y e g => inv(x)*x*y=inv(x)*(x*y)
U Spec, 222
224 x e g => inv(x) e g
U Spec, 7
225 inv(x) e g
Detach, 224, 211
226 inv(x) e g & x e g
Join, 225, 211
227 inv(x) e g & x e g & y e g
Join, 226, 212
228 inv(x)*x*y=inv(x)*(x*y)
Detach, 223, 227
229 inv(x)*x*y=inv(x)*x
Substitute, 228, 215
230 e*y=e
Substitute, 219, 229
Apply defintion of e
231 y e g => y*e=y & e*y=y
U Spec, 6
232 y*e=y & e*y=y
Detach, 231, 212
233 y*e=y
Split, 232
234 e*y=y
Split, 232
235 y=e
Substitute, 234, 230
As Required:
236 x*y=x => y=e
4 Conclusion, 213
As Required:
237 ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
4 Conclusion, 210
Determine identity (left)
*************************
Prove: ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
Suppose
238 x e g & y e g
Premise
239 x e g
Split, 238
240 y e g
Split, 238
Prove: x*y=y => x=e
Suppose...
241 x*y=y
Premise
242 y*inv(y)=y*inv(y)
Reflex
243 x*y*inv(y)=y*inv(y)
Substitute, 241, 242
Apply definition of inv
244 y e g => y*inv(y)=e & inv(y)*y=e
U Spec, 8
245 y*inv(y)=e & inv(y)*y=e
Detach, 244, 240
246 y*inv(y)=e
Split, 245
247 inv(y)*y=e
Split, 245
248 x*y*inv(y)=e
Substitute, 246, 243
Apply associativity
249 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 4
250 ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]
U Spec, 249
251 x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))
U Spec, 250
252 y e g => inv(y) e g
U Spec, 7
253 inv(y) e g
Detach, 252, 240
254 x e g & y e g & inv(y) e g
Join, 238, 253
255 x*y*inv(y)=x*(y*inv(y))
Detach, 251, 254
256 x*(y*inv(y))=e
Substitute, 255, 248
257 x*e=e
Substitute, 246, 256
258 x e g => x*e=x & e*x=x
U Spec, 6
259 x*e=x & e*x=x
Detach, 258, 239
260 x*e=x
Split, 259
261 e*x=x
Split, 259
262 x=e
Substitute, 260, 257
As Required:
263 x*y=y => x=e
4 Conclusion, 241
As Required:
264 ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
4 Conclusion, 238
inv(x*y) = inv(y)*inv(x)
************************
Prove: ALL(a):ALL(b):[a e g & b e g => inv(a*b)=inv(b)*inv(a)]
Suppose...
265 x e g & y e g
Premise
266 x e g
Split, 265
267 y e g
Split, 265
Apply definition of inv
268 x e g => inv(x) e g
U Spec, 7
269 inv(x) e g
Detach, 268, 266
270 y e g => inv(y) e g
U Spec, 7
271 inv(y) e g
Detach, 270, 267
272 x*y*(inv(y)*inv(x))=x*y*(inv(y)*inv(x))
Reflex
Apply associativity of *
273 ALL(b):ALL(c):[x*y e g & b e g & c e g => x*y*b*c=x*y*(b*c)]
U Spec, 4
274 ALL(c):[x*y e g & inv(y) e g & c e g => x*y*inv(y)*c=x*y*(inv(y)*c)]
U Spec, 273
275 x*y e g & inv(y) e g & inv(x) e g => x*y*inv(y)*inv(x)=x*y*(inv(y)*inv(x))
U Spec, 274
276 ALL(b):[x e g & b e g => x*b e g]
U Spec, 3
277 x e g & y e g => x*y e g
U Spec, 276
278 x*y e g
Detach, 277, 265
279 x*y e g & inv(y) e g
Join, 278, 271
280 x*y e g & inv(y) e g & inv(x) e g
Join, 279, 269
281 x*y*inv(y)*inv(x)=x*y*(inv(y)*inv(x))
Detach, 275, 280
282 x*y*(inv(y)*inv(x))=x*y*inv(y)*inv(x)
Substitute, 281, 272
Apply associativity of *
283 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 4
284 ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]
U Spec, 283
285 x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))
U Spec, 284
286 x e g & y e g & inv(y) e g
Join, 265, 271
287 x*y*inv(y)=x*(y*inv(y))
Detach, 285, 286
288 x*y*(inv(y)*inv(x))=x*(y*inv(y))*inv(x)
Substitute, 287, 282
289 y e g => y*inv(y)=e & inv(y)*y=e
U Spec, 8
290 y*inv(y)=e & inv(y)*y=e
Detach, 289, 267
291 y*inv(y)=e
Split, 290
292 inv(y)*y=e
Split, 290
293 x*y*(inv(y)*inv(x))=x*e*inv(x)
Substitute, 291, 288
294 x e g => x*e=x & e*x=x
U Spec, 6
295 x*e=x & e*x=x
Detach, 294, 266
296 x*e=x
Split, 295
297 e*x=x
Split, 295
298 x*y*(inv(y)*inv(x))=x*inv(x)
Substitute, 296, 293
Apply definition of inv
299 x e g => x*inv(x)=e & inv(x)*x=e
U Spec, 8
300 x*inv(x)=e & inv(x)*x=e
Detach, 299, 266
301 x*inv(x)=e
Split, 300
302 inv(x)*x=e
Split, 300
303 x*y*(inv(y)*inv(x))=e
Substitute, 301, 298
Apply previous result
304 ALL(b):[x*y e g & b e g => [x*y*b=e => inv(x*y)=b & inv(b)=x*y]]
U Spec, 198
305 x*y e g & inv(y)*inv(x) e g => [x*y*(inv(y)*inv(x))=e => inv(x*y)=inv(y)*inv(x) & inv(inv(y)*inv(x))=x*y]
U Spec, 304
306 ALL(b):[inv(y) e g & b e g => inv(y)*b e g]
U Spec, 3
307 inv(y) e g & inv(x) e g => inv(y)*inv(x) e g
U Spec, 306
308 inv(y) e g & inv(x) e g
Join, 271, 269
309 inv(y)*inv(x) e g
Detach, 307, 308
310 x*y e g & inv(y)*inv(x) e g
Join, 278, 309
311 x*y*(inv(y)*inv(x))=e => inv(x*y)=inv(y)*inv(x) & inv(inv(y)*inv(x))=x*y
Detach, 305, 310
312 inv(x*y)=inv(y)*inv(x) & inv(inv(y)*inv(x))=x*y
Detach, 311, 303
313 inv(x*y)=inv(y)*inv(x)
Split, 312
As Required:
314 ALL(a):ALL(b):[a e g & b e g => inv(a*b)=inv(b)*inv(a)]
4 Conclusion, 265
315 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
Join, 53, 94
316 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
Join, 315, 237
317 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
Join, 316, 264
318 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
Join, 317, 198
319 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
& inv(e)=e
Join, 318, 209
320 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
& inv(e)=e
& ALL(a):[a e g => inv(inv(a))=a]
Join, 319, 134
321 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
& inv(e)=e
& ALL(a):[a e g => inv(inv(a))=a]
& ALL(a):ALL(b):[a e g & b e g => inv(a*b)=inv(b)*inv(a)]
Join, 320, 314
As Required:
322 ALL(g):ALL(e):ALL(inv):[Set(g)
& ALL(a):ALL(b):[a e g & b e g => a*b e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
=> ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
& inv(e)=e
& ALL(a):[a e g => inv(inv(a))=a]
& ALL(a):ALL(b):[a e g & b e g => inv(a*b)=inv(b)*inv(a)]]
4 Conclusion, 1