THEOREM
*******
Here, we apply the axioms of group theory (lines 1-6) to prove:
1. If x*y = z*y then x=z (right cancellation property of *) (lines 7-46)
2. If x*y = x*z then y=z (left cancellation property of *) (lines 47-83)
3. inv(inv(x))= x (lines 84-115)
4. If x*y = e then inv(x) = y and inv(y) =x (lines 117-172)
5. inv(e)= e (lines 173-183)
This proof was written and machine-verified with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com
GROUP AXIOMS
************
Define: g
g is a set
1 Set(g)
Axiom
Define: * operator
* is closed on g
2 ALL(a):ALL(b):[a e g & b e g => a*b e g]
Axiom
* is associative
3 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
Axiom
Define: e
4 e e g
Axiom
e is the identity element
5 ALL(a):[a e g => a*e=a & e*a=a]
Axiom
Define: inv operator
inv(x) is the inverse of x
6 ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]
Axiom
PROOF
*****
Prove: ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
x*y = z*y
x*y*inv(y) = z*y*inv(y)
x = z
Suppose...
7 x e g & y e g & z e g
Premise
8 x e g
Split, 7
9 y e g
Split, 7
10 z e g
Split, 7
Prove: x*y=z*y => x=z
Suppose...
11 x*y=z*y
Premise
Apply definition of inv
12 y e g => inv(y) e g & y*inv(y)=e & inv(y)*y=e
U Spec, 6
13 inv(y) e g & y*inv(y)=e & inv(y)*y=e
Detach, 12, 9
14 inv(y) e g
Split, 13
15 y*inv(y)=e
Split, 13
16 inv(y)*y=e
Split, 13
17 x*y*inv(y)=x*y*inv(y)
Reflex
18 x*y*inv(y)=z*y*inv(y)
Substitute, 11, 17
Apply associativity
19 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 3
20 ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]
U Spec, 19
21 x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))
U Spec, 20
22 x e g & y e g
Join, 8, 9
23 x e g & y e g & inv(y) e g
Join, 22, 14
24 x*y*inv(y)=x*(y*inv(y))
Detach, 21, 23
25 x*(y*inv(y))=z*y*inv(y)
Substitute, 24, 18
26 x*e=z*y*inv(y)
Substitute, 15, 25
27 x e g => x*e=x & e*x=x
U Spec, 5
28 x*e=x & e*x=x
Detach, 27, 8
29 x*e=x
Split, 28
30 e*x=x
Split, 28
31 x=z*y*inv(y)
Substitute, 29, 26
Apply associativity
32 ALL(b):ALL(c):[z e g & b e g & c e g => z*b*c=z*(b*c)]
U Spec, 3
33 ALL(c):[z e g & y e g & c e g => z*y*c=z*(y*c)]
U Spec, 32
34 z e g & y e g & inv(y) e g => z*y*inv(y)=z*(y*inv(y))
U Spec, 33
35 z e g & y e g
Join, 10, 9
36 z e g & y e g & inv(y) e g
Join, 35, 14
37 z*y*inv(y)=z*(y*inv(y))
Detach, 34, 36
38 x=z*(y*inv(y))
Substitute, 37, 31
39 x=z*e
Substitute, 15, 38
40 z e g => z*e=z & e*z=z
U Spec, 5
41 z*e=z & e*z=z
Detach, 40, 10
42 z*e=z
Split, 41
43 e*z=z
Split, 41
44 x=z
Substitute, 42, 39
As Required:
45 x*y=z*y => x=z
4 Conclusion, 11
Right cancellation
As Required:
46 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
4 Conclusion, 7
Prove: ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
x*y = x*z
inv(x)*x*y = inv(x)*x*z
y = z
Suppose...
47 x e g & y e g & z e g
Premise
48 x e g
Split, 47
49 y e g
Split, 47
50 z e g
Split, 47
Prove: x*y=x*z => y=z
Suppose...
51 x*y=x*z
Premise
Apply definition of inv
52 x e g => inv(x) e g & x*inv(x)=e & inv(x)*x=e
U Spec, 6
53 inv(x) e g & x*inv(x)=e & inv(x)*x=e
Detach, 52, 48
54 inv(x) e g
Split, 53
55 x*inv(x)=e
Split, 53
56 inv(x)*x=e
Split, 53
57 inv(x)*(x*y)=inv(x)*(x*y)
Reflex
58 inv(x)*(x*y)=inv(x)*(x*z)
Substitute, 51, 57
Apply associativity
59 ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]
U Spec, 3
60 ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]
U Spec, 59
61 inv(x) e g & x e g & y e g => inv(x)*x*y=inv(x)*(x*y)
U Spec, 60
62 inv(x) e g & x e g
Join, 54, 48
63 inv(x) e g & x e g & y e g
Join, 62, 49
64 inv(x)*x*y=inv(x)*(x*y)
Detach, 61, 63
65 inv(x)*x*y=inv(x)*(x*z)
Substitute, 64, 58
66 e*y=inv(x)*(x*z)
Substitute, 56, 65
67 y e g => y*e=y & e*y=y
U Spec, 5
68 y*e=y & e*y=y
Detach, 67, 49
69 y*e=y
Split, 68
70 e*y=y
Split, 68
71 y=inv(x)*(x*z)
Substitute, 70, 66
Apply associativity
72 inv(x) e g & x e g & z e g => inv(x)*x*z=inv(x)*(x*z)
U Spec, 60
73 inv(x) e g & x e g & z e g
Join, 62, 50
74 inv(x)*x*z=inv(x)*(x*z)
Detach, 72, 73
75 y=inv(x)*x*z
Substitute, 74, 71
76 y=e*z
Substitute, 56, 75
Apply definition of e
77 z e g => z*e=z & e*z=z
U Spec, 5
78 z*e=z & e*z=z
Detach, 77, 50
79 z*e=z
Split, 78
80 e*z=z
Split, 78
81 y=z
Substitute, 80, 76
As Required:
82 x*y=x*z => y=z
4 Conclusion, 51
Left cancellation
As Required:
83 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
4 Conclusion, 47
Prove: ALL(a):[a e g => inv(inv(a))=a]
Suppose...
84 x e g
Premise
85 x e g => inv(x) e g & x*inv(x)=e & inv(x)*x=e
U Spec, 6
86 inv(x) e g & x*inv(x)=e & inv(x)*x=e
Detach, 85, 84
87 inv(x) e g
Split, 86
88 x*inv(x)=e
Split, 86
89 inv(x)*x=e
Split, 86
Apply definiton of inv
90 inv(x) e g => inv(inv(x)) e g & inv(x)*inv(inv(x))=e & inv(inv(x))*inv(x)=e
U Spec, 6
91 inv(inv(x)) e g & inv(x)*inv(inv(x))=e & inv(inv(x))*inv(x)=e
Detach, 90, 87
92 inv(inv(x)) e g
Split, 91
93 inv(x)*inv(inv(x))=e
Split, 91
94 inv(inv(x))*inv(x)=e
Split, 91
95 e*x=e*x
Reflex
96 inv(inv(x))*inv(x)*x=e*x
Substitute, 94, 95
Apply associativity
97 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, 3
98 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, 97
99 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, 98
100 inv(inv(x)) e g & inv(x) e g
Join, 92, 87
101 inv(inv(x)) e g & inv(x) e g & x e g
Join, 100, 84
102 inv(inv(x))*inv(x)*x=inv(inv(x))*(inv(x)*x)
Detach, 99, 101
103 inv(inv(x))*(inv(x)*x)=e*x
Substitute, 102, 96
104 inv(inv(x))*e=e*x
Substitute, 89, 103
Apply definition of e
105 inv(inv(x)) e g => inv(inv(x))*e=inv(inv(x)) & e*inv(inv(x))=inv(inv(x))
U Spec, 5
106 inv(inv(x))*e=inv(inv(x)) & e*inv(inv(x))=inv(inv(x))
Detach, 105, 92
107 inv(inv(x))*e=inv(inv(x))
Split, 106
108 e*inv(inv(x))=inv(inv(x))
Split, 106
109 inv(inv(x))=e*x
Substitute, 107, 104
110 x e g => x*e=x & e*x=x
U Spec, 5
111 x*e=x & e*x=x
Detach, 110, 84
112 x*e=x
Split, 111
113 e*x=x
Split, 111
114 inv(inv(x))=x
Substitute, 113, 109
As Required:
115 ALL(a):[a e g => inv(inv(a))=a]
4 Conclusion, 84
Prove: ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
Suppose...
116 x e g & y e g
Premise
117 x e g
Split, 116
118 y e g
Split, 116
Prove: x*y=e => inv(x)=y & inv(y)=x
Suppose...
119 x*y=e
Premise
Apply definition of inv
120 x e g => inv(x) e g & x*inv(x)=e & inv(x)*x=e
U Spec, 6
121 inv(x) e g & x*inv(x)=e & inv(x)*x=e
Detach, 120, 117
122 inv(x) e g
Split, 121
123 x*inv(x)=e
Split, 121
124 inv(x)*x=e
Split, 121
125 inv(x)*x*y=inv(x)*x*y
Reflex
126 e*y=inv(x)*x*y
Substitute, 124, 125
Apply definition of e
127 y e g => y*e=y & e*y=y
U Spec, 5
128 y*e=y & e*y=y
Detach, 127, 118
129 y*e=y
Split, 128
130 e*y=y
Split, 128
131 y=inv(x)*x*y
Substitute, 130, 126
Apply associativity
132 ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]
U Spec, 3
133 ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]
U Spec, 132
134 inv(x) e g & x e g & y e g => inv(x)*x*y=inv(x)*(x*y)
U Spec, 133
135 inv(x) e g & x e g
Join, 122, 117
136 inv(x) e g & x e g & y e g
Join, 135, 118
137 inv(x)*x*y=inv(x)*(x*y)
Detach, 134, 136
138 y=inv(x)*(x*y)
Substitute, 137, 131
139 y=inv(x)*e
Substitute, 119, 138
Apply definiton of e
140 inv(x) e g => inv(x)*e=inv(x) & e*inv(x)=inv(x)
U Spec, 5
141 inv(x)*e=inv(x) & e*inv(x)=inv(x)
Detach, 140, 122
142 inv(x)*e=inv(x)
Split, 141
143 e*inv(x)=inv(x)
Split, 141
As Required:
144 y=inv(x)
Substitute, 142, 139
Apply definiton of inv
145 y e g => inv(y) e g & y*inv(y)=e & inv(y)*y=e
U Spec, 6
146 inv(y) e g & y*inv(y)=e & inv(y)*y=e
Detach, 145, 118
147 inv(y) e g
Split, 146
148 y*inv(y)=e
Split, 146
149 inv(y)*y=e
Split, 146
150 x*y*inv(y)=x*y*inv(y)
Reflex
151 e*inv(y)=x*y*inv(y)
Substitute, 119, 150
Apply definition of e
152 inv(y) e g => inv(y)*e=inv(y) & e*inv(y)=inv(y)
U Spec, 5
153 inv(y)*e=inv(y) & e*inv(y)=inv(y)
Detach, 152, 147
154 inv(y)*e=inv(y)
Split, 153
155 e*inv(y)=inv(y)
Split, 153
156 inv(y)=x*y*inv(y)
Substitute, 155, 151
Apply associativity
157 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 3
158 ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]
U Spec, 157
159 x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))
U Spec, 158
160 x e g & y e g & inv(y) e g
Join, 116, 147
161 x*y*inv(y)=x*(y*inv(y))
Detach, 159, 160
162 inv(y)=x*(y*inv(y))
Substitute, 161, 156
163 inv(y)=x*e
Substitute, 148, 162
Apply definition of e
164 x e g => x*e=x & e*x=x
U Spec, 5
165 x*e=x & e*x=x
Detach, 164, 117
166 x*e=x
Split, 165
167 e*x=x
Split, 165
168 inv(y)=x
Substitute, 166, 163
169 inv(x)=y
Sym, 144
170 inv(x)=y & inv(y)=x
Join, 169, 168
As Required:
171 x*y=e => inv(x)=y & inv(y)=x
4 Conclusion, 119
As Required:
172 ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
4 Conclusion, 116
Prove: inv(e)=e
Apply definition of e
173 e e g => e*e=e & e*e=e
U Spec, 5
174 e*e=e & e*e=e
Detach, 173, 4
175 e*e=e
Split, 174
176 e*e=e
Split, 174
Apply previous result
177 ALL(b):[e e g & b e g => [e*b=e => inv(e)=b & inv(b)=e]]
U Spec, 172
178 e e g & e e g => [e*e=e => inv(e)=e & inv(e)=e]
U Spec, 177
179 e e g & e e g
Join, 4, 4
180 e*e=e => inv(e)=e & inv(e)=e
Detach, 178, 179
181 inv(e)=e & inv(e)=e
Detach, 180, 176
182 inv(e)=e
Split, 181
As Required:
183 inv(e)=e
Split, 181