The Left Identity is the Right Identity
---------------------------------------
Prove: ALL(a):[a e g => 0+a=a]
where g is the underlying set that is closed under +
'_' is the right inverse operator
0 is the right identity
Outline:
Let x e g. Applying the axioms of group theory, we have:
0+x = x+_x+x (Inverse)
= x+(_x+x) (Associativity)
= x+0 (Previous Result)
= x (Identity)
Given The Group Axioms
----------------------
G1:
1 Set(g)
Axiom
G2:
2 0 e g
Axiom
G3: Closure
3 ALL(a):ALL(b):[a e g & b e g => a+b e g]
Axiom
G4: Associativity
4 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a+b+c=a+(b+c)]
Axiom
G5: Right Identity
5 ALL(a):[a e g => a+0=a]
Axiom
G6:
6 ALL(a):[a e g => _a e g]
Axiom
G7: Right Inverse
7 ALL(a):[a e g => a+_a=0]
Axiom
Previous result: The left inverse is the right inverse
8 ALL(a):[a e g => _a+a=0]
Axiom
Proof
-----
Suppose...
9 x e g
Premise
Apply G6
10 x e g => _x e g
U Spec, 6
11 _x e g
Detach, 10, 9
Apply G7
12 x e g => x+_x=0
U Spec, 7
13 x+_x=0
Detach, 12, 9
Apply reflexivity
14 0+x=0+x
Reflex
15 0+x=x+_x+x
Substitute, 13, 14
Apply G4
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 & _x e g & c e g => x+_x+c=x+(_x+c)]
U Spec, 16
18 x e g & _x e g & x e g => x+_x+x=x+(_x+x)
U Spec, 17
19 x e g & _x e g
Join, 9, 11
20 x e g & _x e g & x e g
Join, 19, 9
21 x+_x+x=x+(_x+x)
Detach, 18, 20
22 0+x=x+(_x+x)
Substitute, 21, 15
Apply previous result
23 x e g => _x+x=0
U Spec, 8
24 _x+x=0
Detach, 23, 9
25 0+x=x+0
Substitute, 24, 22
Apply G5
26 x e g => x+0=x
U Spec, 5
27 x+0=x
Detach, 26, 9
28 0+x=x
Substitute, 27, 25
As Required:
29 ALL(a):[a e g => 0+a=a]
4 Conclusion, 9
Prove: ALL(a):[a e g => a+0=a & 0+a=a]
Suppose...
30 x e g
Premise
31 x e g => x+0=x
U Spec, 5
32 x+0=x
Detach, 31, 30
33 x e g => 0+x=x
U Spec, 29
34 0+x=x
Detach, 33, 30
35 x+0=x & 0+x=x
Join, 32, 34
As Required:
36 ALL(a):[a e g => a+0=a & 0+a=a]
4 Conclusion, 30