THEOREM
*******
Starting with the usual definition of a group that defines only right-identities and right-inverses, we prove it is equivalent to a definition of a group that defines for right and left identities and inverses.
Given: 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] <--- right-identity only
& ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]] <--- right-inverses only
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] <--- right and left identity
& ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]]]] <--- right and left inverses
This formal proof was written and machine-verified with the aid of the author's free available at http://www.dcproof.com
DEFINITIONS
***********
Define: Group (for fixed operator *)
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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]]
Axiom
'=>'
Suppose...
2 Group(g)
Premise
3 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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]
U Spec, 1
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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]] => Group(g)]
Iff-And, 3
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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]
Split, 4
6 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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]] => Group(g)
Split, 4
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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]
Detach, 5, 2
* is closed on g
8 ALL(a):ALL(b):[a e g & b e g => a*b e g]
Split, 7
* is associative
9 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
Split, 7
Existence of identity element
10 EXIST(e):[e e g & [ALL(a):[a e g => a*e=a] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]
Split, 7
11 e e g & [ALL(a):[a e g => a*e=a] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]
E Spec, 10
Define: e
12 e e g
Split, 11
13 ALL(a):[a e g => a*e=a] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]
Split, 11
e is a right inverse
14 ALL(a):[a e g => a*e=a]
Split, 13
Existence of right inverses
15 ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]
Split, 13
16 x e g
Premise
Prove: x*x=x => x=e
Suppose...
17 x*x=x
Premise
18 x e g => EXIST(b):[b e g & x*b=e]
U Spec, 15
19 EXIST(b):[b e g & x*b=e]
Detach, 18, 16
20 x' e g & x*x'=e
E Spec, 19
21 x' e g
Split, 20
22 x*x'=e
Split, 20
23 x*x*x'=x*x*x'
Reflex
24 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 9
25 ALL(c):[x e g & x e g & c e g => x*x*c=x*(x*c)]
U Spec, 24
26 x e g & x e g & x' e g => x*x*x'=x*(x*x')
U Spec, 25
27 x e g & x e g
Join, 16, 16
28 x e g & x e g & x' e g
Join, 27, 21
29 x*x*x'=x*(x*x')
Detach, 26, 28
30 x*(x*x')=x*x*x'
Substitute, 29, 23
31 x*e=x*x*x'
Substitute, 22, 30
32 x e g => x*e=x
U Spec, 14
33 x*e=x
Detach, 32, 16
34 x=x*x*x'
Substitute, 33, 31
35 x=x*x'
Substitute, 17, 34
36 x=e
Substitute, 22, 35
As Required:
37 x*x=x => x=e
4 Conclusion, 17
Lemma
As Required:
38 ALL(a):[a e g => [a*a=a => a=e]]
4 Conclusion, 16
Prove: ALL(a):ALL(b):[a e g & b e g => [a*b=e => b*a=e]]
Suppose...
39 x e g & x' e g
Premise
40 x e g
Split, 39
41 x' e g
Split, 39
Prove: x*x'=e => x'*x=e
Suppose...
42 x*x'=e
Premise
43 x'*(x*x')=x'*(x*x')
Reflex
44 x'*(x*x')=x'*e
Substitute, 42, 43
45 x' e g => x'*e=x'
U Spec, 14
46 x'*e=x'
Detach, 45, 41
47 x'*(x*x')=x'
Substitute, 46, 44
48 x'*(x*x')*x=x'*(x*x')*x
Reflex
49 x'*(x*x')*x=x'*x
Substitute, 47, 48
50 ALL(b):ALL(c):[x' e g & b e g & c e g => x'*b*c=x'*(b*c)]
U Spec, 9
51 ALL(c):[x' e g & x e g & c e g => x'*x*c=x'*(x*c)]
U Spec, 50
52 x' e g & x e g & x' e g => x'*x*x'=x'*(x*x')
U Spec, 51
53 x' e g & x e g
Join, 41, 40
54 x' e g & x e g & x' e g
Join, 53, 41
55 x'*x*x'=x'*(x*x')
Detach, 52, 54
56 x'*x*x'*x=x'*x
Substitute, 55, 49
57 ALL(b):ALL(c):[x'*x e g & b e g & c e g => x'*x*b*c=x'*x*(b*c)]
U Spec, 9
58 ALL(c):[x'*x e g & x' e g & c e g => x'*x*x'*c=x'*x*(x'*c)]
U Spec, 57
59 x'*x e g & x' e g & x e g => x'*x*x'*x=x'*x*(x'*x)
U Spec, 58
60 ALL(b):[x' e g & b e g => x'*b e g]
U Spec, 8
61 x' e g & x e g => x'*x e g
U Spec, 60
62 x' e g & x e g
Join, 41, 40
63 x'*x e g
Detach, 61, 62
64 x'*x e g & x' e g
Join, 63, 41
65 x'*x e g & x' e g & x e g
Join, 64, 40
66 x'*x*x'*x=x'*x*(x'*x)
Detach, 59, 65
67 x'*x*(x'*x)=x'*x
Substitute, 66, 56
68 x'*x e g => [x'*x*(x'*x)=x'*x => x'*x=e]
U Spec, 38
69 x'*x*(x'*x)=x'*x => x'*x=e
Detach, 68, 63
70 x'*x=e
Detach, 69, 67
As Required:
71 x*x'=e => x'*x=e
4 Conclusion, 42
As Required:
72 ALL(a):ALL(b):[a e g & b e g => [a*b=e => b*a=e]]
4 Conclusion, 39
Prove: ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]
Suppose...
73 x e g
Premise
74 x e g => EXIST(b):[b e g & x*b=e]
U Spec, 15
75 EXIST(b):[b e g & x*b=e]
Detach, 74, 73
76 x' e g & x*x'=e
E Spec, 75
77 x' e g
Split, 76
78 x*x'=e
Split, 76
79 ALL(b):[x e g & b e g => [x*b=e => b*x=e]]
U Spec, 72
80 x e g & x' e g => [x*x'=e => x'*x=e]
U Spec, 79
81 x e g & x' e g
Join, 73, 77
82 x*x'=e => x'*x=e
Detach, 80, 81
83 x'*x=e
Detach, 82, 78
84 x*x'=e & x'*x=e
Join, 78, 83
85 x' e g & [x*x'=e & x'*x=e]
Join, 77, 84
As Required:
86 ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]
4 Conclusion, 73
Prove: ALL(a):[a e g => a*e=a & e*a=a]
Suppose...
87 x e g
Premise
88 x e g => EXIST(b):[b e g & x*b=e]
U Spec, 15
89 EXIST(b):[b e g & x*b=e]
Detach, 88, 87
90 x' e g & x*x'=e
E Spec, 89
91 x' e g
Split, 90
92 x*x'=e
Split, 90
93 e*x=e*x
Reflex
94 e*x=x*x'*x
Substitute, 92, 93
95 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 9
96 ALL(c):[x e g & x' e g & c e g => x*x'*c=x*(x'*c)]
U Spec, 95
97 x e g & x' e g & x e g => x*x'*x=x*(x'*x)
U Spec, 96
98 x e g & x' e g
Join, 87, 91
99 x e g & x' e g & x e g
Join, 98, 87
100 x*x'*x=x*(x'*x)
Detach, 97, 99
101 e*x=x*(x'*x)
Substitute, 100, 94
102 ALL(b):[x e g & b e g => [x*b=e => b*x=e]]
U Spec, 72
103 x e g & x' e g => [x*x'=e => x'*x=e]
U Spec, 102
104 x e g & x' e g
Join, 87, 91
105 x*x'=e => x'*x=e
Detach, 103, 104
106 x'*x=e
Detach, 105, 92
107 e*x=x*e
Substitute, 106, 101
108 x e g => x*e=x
U Spec, 14
109 x*e=x
Detach, 108, 87
110 e*x=x
Substitute, 109, 107
111 x*e=x & e*x=x
Join, 109, 110
As Required:
112 ALL(a):[a e g => a*e=a & e*a=a]
4 Conclusion, 87
113 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, 112, 86
114 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, 12, 113
115 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, 114
116 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, 8, 9
117 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, 116, 115
As Required:
118 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]]]]]]
4 Conclusion, 2
Prove: ALL(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]]]]]
=> Group(g)]
Suppose...
119 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]]]]]
Premise
120 ALL(a):ALL(b):[a e g & b e g => a*b e g]
Split, 119
121 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
Split, 119
122 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, 119
123 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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]
U Spec, 1
124 [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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]] => Group(g)]
Iff-And, 123
125 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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]
Split, 124
Sufficient: For Group(g)
126 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] & ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]] => Group(g)
Split, 124
127 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, 122
128 e e g
Split, 127
129 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, 127
130 ALL(a):[a e g => a*e=a & e*a=a]
Split, 129
131 ALL(a):[a e g => EXIST(b):[b e g & [a*b=e & b*a=e]]]
Split, 129
Prove: ALL(a):[a e g => a*e=a
Suppose...
132 x e g
Premise
Apply premise
133 x e g => x*e=x & e*x=x
U Spec, 130
134 x*e=x & e*x=x
Detach, 133, 132
135 x*e=x
Split, 134
As Required:
136 ALL(a):[a e g => a*e=a]
4 Conclusion, 132
Prove: ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]
Suppose...
137 x e g
Premise
Apply premise
138 x e g => EXIST(b):[b e g & [x*b=e & b*x=e]]
U Spec, 131
139 EXIST(b):[b e g & [x*b=e & b*x=e]]
Detach, 138, 137
140 x' e g & [x*x'=e & x'*x=e]
E Spec, 139
141 x' e g
Split, 140
142 x*x'=e & x'*x=e
Split, 140
143 x*x'=e
Split, 142
144 x'*x=e
Split, 142
145 x' e g & x*x'=e
Join, 141, 143
As Required:
146 ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]
4 Conclusion, 137
147 ALL(a):[a e g => a*e=a]
& ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]
Join, 136, 146
148 e e g
& [ALL(a):[a e g => a*e=a]
& ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]
Join, 128, 147
149 EXIST(e):[e e g
& [ALL(a):[a e g => a*e=a]
& ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]
E Gen, 148
150 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, 120, 121
151 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]
& ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]]]
Join, 150, 149
152 Group(g)
Detach, 126, 151
As Required:
153 ALL(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]]]]]
=> Group(g)]
4 Conclusion, 119
154 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]]]]]] & [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)]]
Join, 118, 153
As Required:
155 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]]]]]]
Iff-And, 154