THEOREM
*******
Most presentations of the
axioms of group theory seem to give both right and left identities and
inverses, which turns out to be somewhat redundant. Here, given the axioms for
group (g,*) with only right identity and inverse, we formally prove that the right
identity and inverses also a left identity and inverse respectively.
Dan Christensen
2023-07-05
2023-07-09
GROUP (g,*) AXIOMS
******************
1 Set(g)
Axiom
G1: * is closed on g
2 ALL(a):ALL(b):[a e g & b e g => a*b e g]
Axiom
G2: * 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
G3: e is a right identity
4 e e g
Axiom
5 ALL(a):[a e g => a*e=a]
Axiom
G4: Right inverses
6 ALL(a):[a e g => EXIST(b):[b e g & a*b=e]]
Axiom
Lemma
Prove: ALL(a):[a e g => [a*a=a => a=e]]
Suppose...
7 x e g
Premise
Prove: x*x=x => x=e
Suppose...
8 x*x=x
Premise
9 x e g => x*e=x
U Spec, 5
10 x*e=x
Detach, 9, 7
11 x=x*e
Sym, 10
12 x e g => EXIST(b):[b e g & x*b=e]
U Spec, 6
13 EXIST(b):[b e g & x*b=e]
Detach, 12, 7
Define: x'
(inverse of x)
14 x' e g & x*x'=e
E Spec, 13
15 x' e g
Split, 14
16 x*x'=e
Split, 14
17 x=x*(x*x')
Substitute, 16,
11
Apply associativity to obtain x*x*x' on RHS
18 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 3
19 ALL(c):[x e g & x e g & c e g => x*x*c=x*(x*c)]
U Spec, 18
20 x e g & x e g & x' e g => x*x*x'=x*(x*x')
U Spec, 19
21 x e g & x e g
Join, 7, 7
22 x e g & x e g & x' e g
Join, 21, 15
23 x*x*x'=x*(x*x')
Detach, 20, 22
24 x=x*x*x'
Substitute, 23,
17
25 x=x*x'
Substitute, 8, 24
As Required:
26 x=e
Substitute, 16,
25
As Required:
27 x*x=x => x=e
4 Conclusion, 8
Lemma
As Required:
28 ALL(a):[a e g => [a*a=a
=> a=e]]
4 Conclusion, 7
Prove: ALL(a):ALL(b):[a e g & b e g =>
[a*b=e => b*a=e]]
Suppose...
29 x e g & y e g
Premise
30 x e g
Split, 29
31 y e g
Split, 29
Prove: x*y=e => y*x=e
Suppose...
32 x*y=e
Premise
33 y e g => y*e=y
U Spec, 5
34 y*e=y
Detach, 33, 31
35 y*(x*y)=y
Substitute, 32,
34
* both sides by x
36 ALL(b):[y e g & b e g => y*b e g]
U Spec, 2
37 y e g & x e g => y*x e g
U Spec, 36
38 y e g & x e g
Join, 31, 30
39 y*x e g
Detach, 37, 38
40 ALL(b):[y e g & b e g => y*b e g]
U Spec, 2
41 y e g & x e g => y*x e g
U Spec, 40
42 y e g & x e g
Join, 31, 30
43 y*x e g
Detach, 41, 42
44 y*x=y*x
Reflex, 43
45 y*(x*y)*x=y*x
Substitute, 35,
44
Apply associativity to obtain y*x*y*x on LHS
46 ALL(b):ALL(c):[y e g & b e g & c e g => y*b*c=y*(b*c)]
U Spec, 3
47 ALL(c):[y e g & x e g & c e g => y*x*c=y*(x*c)]
U Spec, 46
48 y e g & x e g & y e g => y*x*y=y*(x*y)
U Spec, 47
49 y e g & x e g
Join, 31, 30
50 y e g & x e g & y e g
Join, 49, 31
51 y*x*y=y*(x*y)
Detach, 48, 50
As Required:
52 y*x*y*x=y*x
Substitute, 51,
45
Apply associativity to obtain y*x*(y*x) on LHS
53 ALL(b):ALL(c):[y*x e g & b e g & c e g => y*x*b*c=y*x*(b*c)]
U Spec, 3, 43
54 ALL(c):[y*x e g & y e g & c e g => y*x*y*c=y*x*(y*c)]
U Spec, 53
55 y*x e g & y e g & x e g => y*x*y*x=y*x*(y*x)
U Spec, 54
56 y*x e g & y e g
Join, 39, 31
57 y*x e g & y e g & x e g
Join, 56, 30
58 y*x*y*x=y*x*(y*x)
Detach, 55, 57
As Required:
59 y*x*(y*x)=y*x
Substitute, 58,
52
Apply lemma
60 y*x e g => [y*x*(y*x)=y*x => y*x=e]
U Spec, 28, 43
61 y*x*(y*x)=y*x => y*x=e
Detach, 60, 39
62 y*x=e
Detach, 61, 59
As Required:
63 x*y=e => y*x=e
4 Conclusion, 32
As Required:
64 ALL(a):ALL(b):[a e g & b e g => [a*b=e => b*a=e]]
4 Conclusion, 29
Prove: ALL(a):[a e g => e*a=a]
Suppose...
65 x e g
Premise
66 x e g => x*e=x
U Spec, 5
67 x*e=x
Detach, 66, 65
68 x e g => EXIST(b):[b e g & x*b=e]
U Spec, 6
69 EXIST(b):[b e g & x*b=e]
Detach, 68, 65
Define: x'
(right inverse of x)
70 x' e g & x*x'=e
E Spec, 69
71 x' e g
Split, 70
72 x*x'=e
Split, 70
73 ALL(b):[e e g & b e g => e*b e g]
U Spec, 2
74 e e g & x e g => e*x e g
U Spec, 73
75 e e g & x e g
Join, 4, 65
76 e*x e g
Detach, 74, 75
77 e*x=e*x
Reflex, 76
78 e*x=x*x'*x
Substitute, 72,
77
79 e*x=x*x'*(x*e)
Substitute, 67,
78
Apply associativity to obtain x*x'*x*e on RHS
80 x*x' e g
Substitute, 72, 4
81 ALL(b):ALL(c):[x*x' e g & b e g & c e g => x*x'*b*c=x*x'*(b*c)]
U Spec, 3, 80
82 ALL(c):[x*x' e g & x e g & c e g => x*x'*x*c=x*x'*(x*c)]
U Spec, 81
83 x*x' e g & x e g & e e g => x*x'*x*e=x*x'*(x*e)
U Spec, 82
84 x*x' e g & x e g
Join, 80, 65
85 x*x' e g & x e g & e e g
Join, 84, 4
86 x*x'*x*e=x*x'*(x*e)
Detach, 83, 85
As Required:
87 e*x=x*x'*x*e
Substitute, 86,
79
Apply associativity to obtain x*(x'*x)*e on RHS
88 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 3
89 ALL(c):[x e g & x' e g & c e g => x*x'*c=x*(x'*c)]
U Spec, 88
90 x e g & x' e g & x e g => x*x'*x=x*(x'*x)
U Spec, 89
91 x e g & x' e g
Join, 65, 71
92 x e g & x' e g & x e g
Join, 91, 65
93 x*x'*x=x*(x'*x)
Detach, 90, 92
As Required:
94 e*x=x*(x'*x)*e
Substitute, 93,
87
Apply previous result
95 ALL(b):[x e g & b e g => [x*b=e => b*x=e]]
U Spec, 64
96 x e g & x' e g => [x*x'=e => x'*x=e]
97 x e g & x' e g
U Spec, 95
Join, 65, 71
98 x*x'=e => x'*x=e
Detach, 96, 97
99 x'*x=e
Detach, 98, 72
100 e*x=x*e*e
Substitute, 99,
94
101 e*x=x*e
Substitute, 67,
100
As Required:
102 ALL(a):[a e g => e*a=a*e]
4 Conclusion, 65
As Required:
103 ALL(a):ALL(b):[a e g & b e g => [a*b=e => b*a=e]]
&
ALL(a):[a e g => e*a=a*e]
Join, 64, 102