The Left Inverse is the Right Inverse
-------------------------------------
Prove: ALL(a):[aeg => _a+a=0]
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:
_x+x = _x+x+0 (Identity)
= _x+x+(_x+_(_x)) (Inverse)
= _x+(x+(_x+_(_x))) (Associativity)
= _x+(x+_x+_(_x)) (Associativity)
= _x+(0+_(_x)) (Inverse)
= _x+0+_(_x) (Associativity)
= _x+_(_x) (Identity)
= 0 (Inverse)
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
Proof
-----
Suppose...
8 x e g
Premise
Apply G6
9 x e g => _x e g
U Spec, 6
10 _x e g
Detach, 9, 8
Apply G6
11 _x e g => _(_x) e g
U Spec, 6
12 _(_x) e g
Detach, 11, 10
Apply G7
13 x e g => x+_x=0
U Spec, 7
14 x+_x=0
Detach, 13, 8
Apply G7
15 _x e g => _x+_(_x)=0
U Spec, 7
16 _x+_(_x)=0
Detach, 15, 10
Apply G5
17 _x+x e g => _x+x+0=_x+x
U Spec, 5
Apply G3
18 ALL(b):[_x e g & b e g => _x+b e g]
U Spec, 3
19 _x e g & x e g => _x+x e g
U Spec, 18
20 _x e g & x e g
Join, 10, 8
21 _x+x e g
Detach, 19, 20
22 _x+x+0=_x+x
Detach, 17, 21
23 _x+x=_x+x+0
Sym, 22
24 _x+x=_x+x+(_x+_(_x))
Substitute, 16, 23
Apply G4
25 ALL(b):ALL(c):[_x e g & b e g & c e g => _x+b+c=_x+(b+c)]
U Spec, 4
26 ALL(c):[_x e g & x e g & c e g => _x+x+c=_x+(x+c)]
U Spec, 25
27 _x e g & x e g & _x+_(_x) e g => _x+x+(_x+_(_x))=_x+(x+(_x+_(_x)))
U Spec, 26
28 ALL(b):[_x e g & b e g => _x+b e g]
U Spec, 3
29 _x e g & _(_x) e g => _x+_(_x) e g
U Spec, 28
30 _x e g & _(_x) e g
Join, 10, 12
31 _x+_(_x) e g
Detach, 29, 30
32 _x e g & x e g
Join, 10, 8
33 _x e g & x e g & _x+_(_x) e g
Join, 32, 31
34 _x+x+(_x+_(_x))=_x+(x+(_x+_(_x)))
Detach, 27, 33
35 _x+x=_x+(x+(_x+_(_x)))
Substitute, 34, 24
Apply G4
36 ALL(b):ALL(c):[x e g & b e g & c e g => x+b+c=x+(b+c)]
U Spec, 4
37 ALL(c):[x e g & _x e g & c e g => x+_x+c=x+(_x+c)]
U Spec, 36
38 x e g & _x e g & _(_x) e g => x+_x+_(_x)=x+(_x+_(_x))
U Spec, 37
39 x e g & _x e g
Join, 8, 10
40 x e g & _x e g & _(_x) e g
Join, 39, 12
41 x+_x+_(_x)=x+(_x+_(_x))
Detach, 38, 40
42 _x+x=_x+(x+_x+_(_x))
Substitute, 41, 35
43 _x+x=_x+(0+_(_x))
Substitute, 14, 42
Apply G4
44 ALL(b):ALL(c):[_x e g & b e g & c e g => _x+b+c=_x+(b+c)]
U Spec, 4
45 ALL(c):[_x e g & 0 e g & c e g => _x+0+c=_x+(0+c)]
U Spec, 44
46 _x e g & 0 e g & _(_x) e g => _x+0+_(_x)=_x+(0+_(_x))
U Spec, 45
47 _x e g & 0 e g
Join, 10, 2
48 _x e g & 0 e g & _(_x) e g
Join, 47, 12
49 _x+0+_(_x)=_x+(0+_(_x))
Detach, 46, 48
50 _x+x=_x+0+_(_x)
Substitute, 49, 43
Apply G5
51 _x e g => _x+0=_x
U Spec, 5
52 _x+0=_x
Detach, 51, 10
53 _x+x=_x+_(_x)
Substitute, 52, 50
54 _x+x=0
Substitute, 16, 53
As Required:
55 ALL(a):[a e g => _a+a=0]
4 Conclusion, 8
Prove: ALL(a):[a e g => a+_a=0 & _a+a=0]
56 x e g
Premise
57 x e g => x+_x=0
U Spec, 7
58 x+_x=0
Detach, 57, 56
59 x e g => _x+x=0
U Spec, 55
60 _x+x=0
Detach, 59, 56
61 x+_x=0 & _x+x=0
Join, 58, 60
As Required:
62 ALL(a):[a e g => a+_a=0 & _a+a=0]
4 Conclusion, 56