Group Identities
Prove: For all groups (g,+) with identity 0, if x+z=x or z+x=x then z=0
Let (g,+) be an arbitary group
1 Set(g)
& 0
g
& ALL(a):ALL(b):[ag & bg => a+bg]
& ALL(a):ALL(b):ALL(c):[ag & bg & cg => a+b+c=a+(b+c)]
& ALL(a):[ag => 0+a=a & a+0=a]
& ALL(a):[ag => _ag]
& ALL(a):[ag => a+_a=0 & _a+a=0]
Premise
Splitting this premise...
2 Set(g)
Split, 1
3 0g
Split, 1
Closure of + operator
4 ALL(a):ALL(b):[ag & bg => a+bg]
Split, 1
Associativity of +
5 ALL(a):ALL(b):ALL(c):[ag & bg & cg => a+b+c=a+(b+c)]
Split, 1
Identity element 0
6 ALL(a):[ag => 0+a=a & a+0=a]
Split, 1
Closure of _ operator
7 ALL(a):[ag => _ag]
Split, 1
Inverse operator _
8 ALL(a):[ag => a+_a=0 & _a+a=0]
Split, 1
Prove: xg & zg & [x+z=x | z+x=x] => z=0
Suppose...
9 xg & zg & [x+z=x | z+x=x]
Premise
10 xg
Split, 9
11 zg
Split, 9
We have two cases:
12 x+z=x | z+x=x
Split, 9
Case 1:
Prove: x+z=x => z=0
Suppose...
13 x+z=x
Premise
Applying identity axiom...
14 xg => 0+x=x & x+0=x
U Spec, 6
15 0+x=x & x+0=x
Detach, 14, 10
16 0+x=x
Split, 15
From identity axiom...
17 x+0=x
Split, 15
Substituting...
18 x+z+0=x
Substitute, 13, 17
Applying closure of _ ...
19 xg => _xg
U Spec, 7
20 _xg
Detach, 19, 10
Applying inverse axiom...
21 xg => x+_x=0 & _x+x=0
U Spec, 8
22 x+_x=0 & _x+x=0
Detach, 21, 10
23 x+_x=0
Split, 22
24 _x+x=0
Split, 22
Substituting
25 _x+(x+z+0)=0
Substitute, 18, 24
Applying associativity...
26 ALL(b):ALL(c):[_xg & bg & cg => _x+b+c=_x+(b+c)]
U Spec, 5
Applying closure of +...
27 ALL(b):[xg & bg => x+bg]
U Spec, 4
28 xg & zg => x+zg
U Spec, 27
29 xg & zg
Join, 10, 11
30 x+zg
Detach, 28, 29
31 ALL(c):[_xg & x+zg & cg => _x+(x+z)+c=_x+(x+z+c)]
U Spec, 26
32 _xg & x+zg & 0g => _x+(x+z)+0=_x+(x+z+0)
U Spec, 31
33 _xg & x+zg
Join, 20, 30
34 _xg & x+zg & 0g
Join, 33, 3
35 _x+(x+z)+0=_x+(x+z+0)
Detach, 32, 34
From associativity...
36 _x+(x+z)+0=0
Substitute, 35, 25
Applying identity axiom...
37 _x+(x+z)g => 0+(_x+(x+z))=_x+(x+z) & _x+(x+z)+0=_x+(x+z)
U Spec, 6
38 ALL(b):[_xg & bg => _x+bg]
U Spec, 4
39 _xg & x+zg => _x+(x+z)g
U Spec, 38
40 _xg & x+zg
Join, 20, 30
41 _x+(x+z)g
Detach, 39, 40
42 0+(_x+(x+z))=_x+(x+z) & _x+(x+z)+0=_x+(x+z)
Detach, 37, 41
43 0+(_x+(x+z))=_x+(x+z)
Split, 42
From identity axiom...
44 _x+(x+z)+0=_x+(x+z)
Split, 42
Substituting...
45 _x+(x+z)=0
Substitute, 44, 36
Applying associativity...
46 ALL(b):ALL(c):[_xg & bg & cg => _x+b+c=_x+(b+c)]
U Spec, 5
47 ALL(c):[_xg & xg & cg => _x+x+c=_x+(x+c)]
U Spec, 46
48 _xg & xg & zg => _x+x+z=_x+(x+z)
U Spec, 47
49 _xg & xg
Join, 20, 10
50 _xg & xg & zg
Join, 49, 11
From associativity...
51 _x+x+z=_x+(x+z)
Detach, 48, 50
Substituting...
52 _x+x+z=0
Substitute, 51, 45
Applying inverse axiom...
53 xg => x+_x=0 & _x+x=0
U Spec, 8
54 x+_x=0 & _x+x=0
Detach, 53, 10
55 x+_x=0
Split, 54
From inverse axiom...
56 _x+x=0
Split, 54
Substituting...
57 0+z=0
Substitute, 56, 52
Applying identity axiom....
58 zg => 0+z=z & z+0=z
U Spec, 6
59 0+z=z & z+0=z
Detach, 58, 11
60 0+z=z
Split, 59
From identity axiom...
61 z+0=z
Split, 59
Substituting...
62 z=0
Substitute, 60, 57
Case 1:
63 x+z=x => z=0
Conclusion, 13
Case 2:
Prove: z+x=x => z=0
Suppose...
64 z+x=x
Premise
65 xg => 0+x=x & x+0=x
U Spec, 6
66 0+x=x & x+0=x
Detach, 65, 10
67 0+x=x
Split, 66
68 x+0=x
Split, 66
69 0+(z+x)=x
Substitute, 64, 67
70 xg => _xg
U Spec, 7
71 _xg
Detach, 70, 10
72 xg => x+_x=0 & _x+x=0
U Spec, 8
73 x+_x=0 & _x+x=0
Detach, 72, 10
74 x+_x=0
Split, 73
75 _x+x=0
Split, 73
76 0+(z+x)+_x=0
Substitute, 69, 74
77 ALL(b):ALL(c):[0g & bg & cg => 0+b+c=0+(b+c)]
U Spec, 5
78 ALL(c):[0g & z+xg & cg => 0+(z+x)+c=0+(z+x+c)]
U Spec, 77
79 0g & z+xg & _xg => 0+(z+x)+_x=0+(z+x+_x)
U Spec, 78
80 ALL(b):[zg & bg => z+bg]
U Spec, 4
81 zg & xg => z+xg
U Spec, 80
82 zg & xg
Join, 11, 10
83 z+xg
Detach, 81, 82
84 0g & z+xg
Join, 3, 83
85 0g & z+xg & _xg
Join, 84, 71
86 0+(z+x)+_x=0+(z+x+_x)
Detach, 79, 85
87 0+(z+x+_x)=0
Substitute, 86, 76
88 z+x+_xg => 0+(z+x+_x)=z+x+_x & z+x+_x+0=z+x+_x
U Spec, 6
89 ALL(b):[z+xg & bg => z+x+bg]
U Spec, 4
90 z+xg & _xg => z+x+_xg
U Spec, 89
91 z+xg & _xg
Join, 83, 71
92 z+x+_xg
Detach, 90, 91
93 0+(z+x+_x)=z+x+_x & z+x+_x+0=z+x+_x
Detach, 88, 92
94 0+(z+x+_x)=z+x+_x
Split, 93
95 z+x+_x+0=z+x+_x
Split, 93
96 z+x+_x=0
Substitute, 94, 87
97 ALL(b):ALL(c):[zg & bg & cg => z+b+c=z+(b+c)]
U Spec, 5
98 ALL(c):[zg & xg & cg => z+x+c=z+(x+c)]
U Spec, 97
99 zg & xg & _xg => z+x+_x=z+(x+_x)
U Spec, 98
100 zg & xg
Join, 11, 10
101 zg & xg & _xg
Join, 100, 71
102 z+x+_x=z+(x+_x)
Detach, 99, 101
103 z+(x+_x)=0
Substitute, 102, 96
104 xg => x+_x=0 & _x+x=0
U Spec, 8
105 x+_x=0 & _x+x=0
Detach, 104, 10
106 x+_x=0
Split, 105
107 _x+x=0
Split, 105
108 z+0=0
Substitute, 106, 103
109 zg => 0+z=z & z+0=z
U Spec, 6
110 0+z=z & z+0=z
Detach, 109, 11
111 0+z=z
Split, 110
112 z+0=z
Split, 110
113 z=0
Substitute, 112, 108
Case 2:
114 z+x=x => z=0
Conclusion, 64
Applying Case Rule...
115 [x+z=x => z=0] & [z+x=x => z=0]
Join, 63, 114
116 z=0
Cases, 12, 115
As Required:
117 xg & zg & [x+z=x | z+x=x] => z=0
Conclusion, 9
Generalizing...
118 ALL(z):[xg & zg & [x+z=x | z+x=x] => z=0]
U Gen, 117
119 ALL(x):ALL(z):[xg & zg & [x+z=x | z+x=x] => z=0]
U Gen, 118
For arbitary group (g,+)...
120 Set(g)
& 0g
& ALL(a):ALL(b):[ag & bg => a+bg]
& ALL(a):ALL(b):ALL(c):[ag & bg & cg => a+b+c=a+(b+c)]
& ALL(a):[ag => 0+a=a & a+0=a]
& ALL(a):[ag => _ag]
& ALL(a):[ag => a+_a=0 & _a+a=0]
=> ALL(x):ALL(z):[xg & zg & [x+z=x | z+x=x] => z=0]
Conclusion, 1
Generalizing...
121 ALL(0):[Set(g)
& 0g
& ALL(a):ALL(b):[ag & bg => a+bg]
& ALL(a):ALL(b):ALL(c):[ag & bg & cg => a+b+c=a+(b+c)]
& ALL(a):[ag => 0+a=a & a+0=a]
& ALL(a):[ag => _ag]
& ALL(a):[ag => a+_a=0 & _a+a=0]
=> ALL(x):ALL(z):[xg & zg & [x+z=x | z+x=x] => z=0]]
U Gen, 120
As Required:
Generalizing...
122 ALL(g):ALL(0):[Set(g)
& 0g
& ALL(a):ALL(b):[ag & bg => a+bg]
& ALL(a):ALL(b):ALL(c):[ag & bg & cg => a+b+c=a+(b+c)]
& ALL(a):[ag => 0+a=a & a+0=a]
& ALL(a):[ag => _ag]
& ALL(a):[ag => a+_a=0 & _a+a=0]
=> ALL(x):ALL(z):[xg & zg & [x+z=x | z+x=x] => z=0]]
U Gen, 121