THEOREM
*******
Introducing an equivalent definition of a group that defines an inverse function inv: G --> G
Given: Group(g) <=> ALL(a):ALL(b):[a e g & b e g => a*b e g] (Previous result, link below)
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]
Prove: Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]] <--- inv function on G
This formal proof was written and machine-verfied with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com
PREVIOUS RESULT
***************
Definition of group with right and left identity and inverse elements (See proof)
1 ALL(g):[Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]]
Axiom
Suppose g is a set (used to construct inv function)
2 Set(g)
Premise
'=>'
Suppose...
3 Group(g)
Premise
Apply previous result
4 Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]
U Spec, 1
5 [Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]]
& [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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]] => Group(g)]
Iff-And, 4
6 Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]
Split, 5
7 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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]] => Group(g)
Split, 5
8 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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]
Detach, 6, 3
9 ALL(a):ALL(b):[a e g & b e g => a*b e g]
Split, 8
10 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
Split, 8
11 EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]
Split, 8
12 e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]
E Spec, 11
13 e e g
Split, 12
14 ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]
Split, 12
15 ALL(a):[a e g => a*e=a & e*a=a]
Split, 14
16 ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]
Split, 14
Construct g2
Apply Cartesian Product Axiom
17 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
18 ALL(a2):[Set(g) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e g & c2 e a2]]]
U Spec, 17
19 Set(g) & Set(g) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e g & c2 e g]]
U Spec, 18
20 Set(g) & Set(g)
Join, 2, 2
21 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e g & c2 e g]]
Detach, 19, 20
22 Set'(g2) & ALL(c1):ALL(c2):[(c1,c2) e g2 <=> c1 e g & c2 e g]
E Spec, 21
Define: g2
23 Set'(g2)
Split, 22
24 ALL(c1):ALL(c2):[(c1,c2) e g2 <=> c1 e g & c2 e g]
Split, 22
Construct inv
Apply Subset Axiom
25 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e g2 & a*b=e]]
Subset, 23
26 Set'(inv) & ALL(a):ALL(b):[(a,b) e inv <=> (a,b) e g2 & a*b=e]
E Spec, 25
Define: inv
27 Set'(inv)
Split, 26
28 ALL(a):ALL(b):[(a,b) e inv <=> (a,b) e g2 & a*b=e]
Split, 26
Prove: inv is a function
Apply Function Axiom
29 ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]]
Function
30 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e inv => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e inv]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]
=> ALL(c):ALL(d):[d=inv(c) <=> (c,d) e inv]]
U Spec, 29
31 ALL(b):[ALL(c):ALL(d):[(c,d) e inv => c e g & d e b]
& ALL(c):[c e g => EXIST(d):[d e b & (c,d) e inv]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]
=> ALL(c):ALL(d):[d=inv(c) <=> (c,d) e inv]]
U Spec, 30
Sufficient: For functionality of inv
32 ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]
& ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]
=> ALL(c):ALL(d):[d=inv(c) <=> (c,d) e inv]
U Spec, 31
Prove: ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]
Suppose...
33 (x,y) e inv
Premise
Apply definition of inv
34 ALL(b):[(x,b) e inv <=> (x,b) e g2 & x*b=e]
U Spec, 28
35 (x,y) e inv <=> (x,y) e g2 & x*y=e
U Spec, 34
36 [(x,y) e inv => (x,y) e g2 & x*y=e]
& [(x,y) e g2 & x*y=e => (x,y) e inv]
Iff-And, 35
37 (x,y) e inv => (x,y) e g2 & x*y=e
Split, 36
38 (x,y) e g2 & x*y=e => (x,y) e inv
Split, 36
39 (x,y) e g2 & x*y=e
Detach, 37, 33
40 (x,y) e g2
Split, 39
41 x*y=e
Split, 39
Apply definition of g2
42 ALL(c2):[(x,c2) e g2 <=> x e g & c2 e g]
U Spec, 24
43 (x,y) e g2 <=> x e g & y e g
U Spec, 42
44 [(x,y) e g2 => x e g & y e g]
& [x e g & y e g => (x,y) e g2]
Iff-And, 43
45 (x,y) e g2 => x e g & y e g
Split, 44
46 x e g & y e g => (x,y) e g2
Split, 44
47 x e g & y e g
Detach, 45, 40
Functionality, Part 1
As Required:
48 ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]
4 Conclusion, 33
Prove: ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]
Suppose...
49 x e g
Premise
Apply premise
50 x e g => EXIST(b):[b e g & [x*b=e & b*x=e]]
U Spec, 16
51 EXIST(b):[b e g & [x*b=e & b*x=e]]
Detach, 50, 49
52 x' e g & [x*x'=e & x'*x=e]
E Spec, 51
53 x' e g
Split, 52
54 x*x'=e & x'*x=e
Split, 52
55 x*x'=e
Split, 54
56 x'*x=e
Split, 54
Apply definiton of inv
57 ALL(b):[(x,b) e inv <=> (x,b) e g2 & x*b=e]
U Spec, 28
58 (x,x') e inv <=> (x,x') e g2 & x*x'=e
U Spec, 57
59 [(x,x') e inv => (x,x') e g2 & x*x'=e]
& [(x,x') e g2 & x*x'=e => (x,x') e inv]
Iff-And, 58
60 (x,x') e inv => (x,x') e g2 & x*x'=e
Split, 59
61 (x,x') e g2 & x*x'=e => (x,x') e inv
Split, 59
62 ALL(c2):[(x,c2) e g2 <=> x e g & c2 e g]
U Spec, 24
Apply definition of g2
63 (x,x') e g2 <=> x e g & x' e g
U Spec, 62
64 [(x,x') e g2 => x e g & x' e g]
& [x e g & x' e g => (x,x') e g2]
Iff-And, 63
65 (x,x') e g2 => x e g & x' e g
Split, 64
66 x e g & x' e g => (x,x') e g2
Split, 64
67 x e g & x' e g
Join, 49, 53
68 (x,x') e g2
Detach, 66, 67
69 (x,x') e g2 & x*x'=e
Join, 68, 55
70 (x,x') e inv
Detach, 61, 69
71 x' e g & (x,x') e inv
Join, 53, 70
Functionality, Part 2
As Required:
72 ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]
4 Conclusion, 49
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]
Suppose...
73 (x,y1) e inv & (x,y2) e inv
Premise
74 (x,y1) e inv
Split, 73
75 (x,y2) e inv
Split, 73
Apply definition of inv
76 ALL(b):[(x,b) e inv <=> (x,b) e g2 & x*b=e]
U Spec, 28
77 (x,y1) e inv <=> (x,y1) e g2 & x*y1=e
U Spec, 76
78 [(x,y1) e inv => (x,y1) e g2 & x*y1=e]
& [(x,y1) e g2 & x*y1=e => (x,y1) e inv]
Iff-And, 77
79 (x,y1) e inv => (x,y1) e g2 & x*y1=e
Split, 78
80 (x,y1) e g2 & x*y1=e => (x,y1) e inv
Split, 78
81 (x,y1) e g2 & x*y1=e
Detach, 79, 74
82 (x,y1) e g2
Split, 81
83 x*y1=e
Split, 81
Apply definition of g2
84 ALL(c2):[(x,c2) e g2 <=> x e g & c2 e g]
U Spec, 24
85 (x,y1) e g2 <=> x e g & y1 e g
U Spec, 84
86 [(x,y1) e g2 => x e g & y1 e g]
& [x e g & y1 e g => (x,y1) e g2]
Iff-And, 85
87 (x,y1) e g2 => x e g & y1 e g
Split, 86
88 x e g & y1 e g => (x,y1) e g2
Split, 86
89 x e g & y1 e g
Detach, 87, 82
90 x e g
Split, 89
91 y1 e g
Split, 89
Apply definition of inv
92 (x,y2) e inv <=> (x,y2) e g2 & x*y2=e
U Spec, 76
93 [(x,y2) e inv => (x,y2) e g2 & x*y2=e]
& [(x,y2) e g2 & x*y2=e => (x,y2) e inv]
Iff-And, 92
94 (x,y2) e inv => (x,y2) e g2 & x*y2=e
Split, 93
95 (x,y2) e g2 & x*y2=e => (x,y2) e inv
Split, 93
96 (x,y2) e g2 & x*y2=e
Detach, 94, 75
97 (x,y2) e g2
Split, 96
98 x*y2=e
Split, 96
Apply definition of g2
99 (x,y2) e g2 <=> x e g & y2 e g
U Spec, 84
100 [(x,y2) e g2 => x e g & y2 e g]
& [x e g & y2 e g => (x,y2) e g2]
Iff-And, 99
101 (x,y2) e g2 => x e g & y2 e g
Split, 100
102 x e g & y2 e g => (x,y2) e g2
Split, 100
103 x e g & y2 e g
Detach, 101, 97
104 x e g
Split, 103
105 y2 e g
Split, 103
106 x*y1=x*y2
Substitute, 98, 83
Apply premise
107 x e g => EXIST(b):[b e g & [x*b=e & b*x=e]]
U Spec, 16
108 EXIST(b):[b e g & [x*b=e & b*x=e]]
Detach, 107, 90
109 x' e g & [x*x'=e & x'*x=e]
E Spec, 108
110 x' e g
Split, 109
111 x*x'=e & x'*x=e
Split, 109
112 x*x'=e
Split, 111
113 x'*x=e
Split, 111
114 x'*x*y1=x'*x*y1
Reflex
115 e*y1=x'*x*y1
Substitute, 113, 114
Apply premise
116 y1 e g => y1*e=y1 & e*y1=y1
U Spec, 15
117 y1*e=y1 & e*y1=y1
Detach, 116, 91
118 y1*e=y1
Split, 117
119 e*y1=y1
Split, 117
120 y1=x'*x*y1
Substitute, 119, 115
Apply associativity
121 ALL(b):ALL(c):[x' e g & b e g & c e g => x'*b*c=x'*(b*c)]
U Spec, 10
122 ALL(c):[x' e g & x e g & c e g => x'*x*c=x'*(x*c)]
U Spec, 121
123 x' e g & x e g & y1 e g => x'*x*y1=x'*(x*y1)
U Spec, 122
124 x' e g & x e g
Join, 110, 90
125 x' e g & x e g & y1 e g
Join, 124, 91
126 x'*x*y1=x'*(x*y1)
Detach, 123, 125
127 y1=x'*(x*y1)
Substitute, 126, 120
128 y1=x'*(x*y2)
Substitute, 106, 127
Apply associativity
129 x' e g & x e g & y2 e g => x'*x*y2=x'*(x*y2)
U Spec, 122
130 x' e g & x e g & y2 e g
Join, 124, 105
131 x'*x*y2=x'*(x*y2)
Detach, 129, 130
132 y1=x'*x*y2
Substitute, 131, 128
133 y1=e*y2
Substitute, 113, 132
134 y2 e g => y2*e=y2 & e*y2=y2
U Spec, 15
135 y2*e=y2 & e*y2=y2
Detach, 134, 105
136 y2*e=y2
Split, 135
137 e*y2=y2
Split, 135
138 y1=y2
Substitute, 137, 133
Functionality, Part 3
As Required:
139 ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]
4 Conclusion, 73
Joining results...
140 ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]
& ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]
Join, 48, 72
141 ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]
& ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]
Join, 140, 139
inv is a function
As Required:
142 ALL(c):ALL(d):[d=inv(c) <=> (c,d) e inv]
Detach, 32, 141
Prove: ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]
Suppose...
143 x e g
Premise
Apply premise
144 x e g => EXIST(b):[b e g & [x*b=e & b*x=e]]
U Spec, 16
145 EXIST(b):[b e g & [x*b=e & b*x=e]]
Detach, 144, 143
146 x' e g & [x*x'=e & x'*x=e]
E Spec, 145
147 x' e g
Split, 146
148 x*x'=e & x'*x=e
Split, 146
149 x*x'=e
Split, 148
150 x'*x=e
Split, 148
Apply definition inv
151 ALL(b):[(x,b) e inv <=> (x,b) e g2 & x*b=e]
U Spec, 28
152 (x,x') e inv <=> (x,x') e g2 & x*x'=e
U Spec, 151
153 [(x,x') e inv => (x,x') e g2 & x*x'=e]
& [(x,x') e g2 & x*x'=e => (x,x') e inv]
Iff-And, 152
154 (x,x') e inv => (x,x') e g2 & x*x'=e
Split, 153
155 (x,x') e g2 & x*x'=e => (x,x') e inv
Split, 153
Apply definition of g2
156 ALL(c2):[(x,c2) e g2 <=> x e g & c2 e g]
U Spec, 24
157 (x,x') e g2 <=> x e g & x' e g
U Spec, 156
158 [(x,x') e g2 => x e g & x' e g]
& [x e g & x' e g => (x,x') e g2]
Iff-And, 157
159 (x,x') e g2 => x e g & x' e g
Split, 158
160 x e g & x' e g => (x,x') e g2
Split, 158
161 x e g & x' e g
Join, 143, 147
162 (x,x') e g2
Detach, 160, 161
163 (x,x') e g2 & x*x'=e
Join, 162, 149
164 (x,x') e inv
Detach, 155, 163
Apply definition of inv
165 ALL(b):[(x',b) e inv <=> (x',b) e g2 & x'*b=e]
U Spec, 28
166 (x',x) e inv <=> (x',x) e g2 & x'*x=e
U Spec, 165
167 [(x',x) e inv => (x',x) e g2 & x'*x=e]
& [(x',x) e g2 & x'*x=e => (x',x) e inv]
Iff-And, 166
168 (x',x) e inv => (x',x) e g2 & x'*x=e
Split, 167
169 (x',x) e g2 & x'*x=e => (x',x) e inv
Split, 167
Apply definition of g2
170 ALL(c2):[(x',c2) e g2 <=> x' e g & c2 e g]
U Spec, 24
171 (x',x) e g2 <=> x' e g & x e g
U Spec, 170
172 [(x',x) e g2 => x' e g & x e g]
& [x' e g & x e g => (x',x) e g2]
Iff-And, 171
173 (x',x) e g2 => x' e g & x e g
Split, 172
174 x' e g & x e g => (x',x) e g2
Split, 172
175 x' e g & x e g
Join, 147, 143
176 (x',x) e g2
Detach, 174, 175
177 (x',x) e g2 & x'*x=e
Join, 176, 150
178 (x',x) e inv
Detach, 169, 177
Apply functionality of inv
179 ALL(d):[d=inv(x) <=> (x,d) e inv]
U Spec, 142
180 x'=inv(x) <=> (x,x') e inv
U Spec, 179
181 [x'=inv(x) => (x,x') e inv]
& [(x,x') e inv => x'=inv(x)]
Iff-And, 180
182 x'=inv(x) => (x,x') e inv
Split, 181
183 (x,x') e inv => x'=inv(x)
Split, 181
184 x'=inv(x)
Detach, 183, 164
Apply fuctionality of inv
185 ALL(d):[d=inv(x') <=> (x',d) e inv]
U Spec, 142
186 x=inv(x') <=> (x',x) e inv
U Spec, 185
187 [x=inv(x') => (x',x) e inv]
& [(x',x) e inv => x=inv(x')]
Iff-And, 186
188 x=inv(x') => (x',x) e inv
Split, 187
189 (x',x) e inv => x=inv(x')
Split, 187
190 x=inv(x')
Detach, 189, 178
191 x*inv(x)=e
Substitute, 184, 149
192 inv(x)*x=e
Substitute, 184, 150
193 inv(x) e g
Substitute, 184, 147
194 inv(x) e g & x*inv(x)=e
Join, 193, 191
195 inv(x) e g & x*inv(x)=e & inv(x)*x=e
Join, 194, 192
As Required:
196 ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]
4 Conclusion, 143
Generalizing...
197 EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]
E Gen, 196
Joining results...
198 ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]
Join, 15, 197
199 e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]
Join, 13, 198
Generalizing...
200 EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]
E Gen, 199
Joining results...
201 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)]
Join, 9, 10
202 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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]
Join, 201, 200
As Required:
203 Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]
4 Conclusion, 3
'<='
Prove: 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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]
=> Group(g)
Suppose...
204 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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]
Premise
205 ALL(a):ALL(b):[a e g & b e g => a*b e g]
Split, 204
206 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
Split, 204
207 EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]
Split, 204
208 e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]
E Spec, 207
209 e e g
Split, 208
210 ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]
Split, 208
211 ALL(a):[a e g => a*e=a & e*a=a]
Split, 210
212 EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]
Split, 210
Apply premise
213 Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]
U Spec, 1
214 [Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]]
& [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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]] => Group(g)]
Iff-And, 213
215 Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]
Split, 214
Sufficient: For Group(g)
216 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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]] => Group(g)
Split, 214
Prove: ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]
Suppose...
217 x e g
Premise
Apply premise
218 ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]
E Spec, 212
219 x e g => inv(x) e g & x*inv(x)=e & inv(x)*x=e
U Spec, 218
220 inv(x) e g & x*inv(x)=e & inv(x)*x=e
Detach, 219, 217
221 inv(x) e g
Split, 220
222 x*inv(x)=e
Split, 220
223 inv(x)*x=e
Split, 220
224 x*inv(x)=e & inv(x)*x=e
Join, 222, 223
225 inv(x) e g & [x*inv(x)=e & inv(x)*x=e]
Join, 221, 224
226 EXIST(b):[b e g & [x*b=e & b*x=e]]
E Gen, 225
As Required:
227 ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]
4 Conclusion, 217
Joining results...
228 ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]
Join, 211, 227
229 e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]
Join, 209, 228
Generalizing...
230 EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]
E Gen, 229
231 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)]
Join, 205, 206
232 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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]
Join, 231, 230
233 Group(g)
Detach, 216, 232
As Required:
234 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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]
=> Group(g)
4 Conclusion, 204
Joining '=>' and '<=' to obtain '<=>'
235 [Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]]
& [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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]
=> Group(g)]
Join, 203, 234
As Required:
236 Group(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)]
& EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a & e*a=a]
& EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]]
Iff-And, 235