THEOREM
*******
Suppose (g,*) is a group and h is a non-empty, finite subset of g. Then (h,*) is a subgroup of (g,*) if and only if * is closed on h.
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 available at http://www.dcproof.com
DEFINITIONS
***********
Define: Group
Group(g,e,inv) means that (g,*) is a group with identity e and inverse operator inv
1 ALL(g):ALL(e):ALL(inv):[Group(g,e,inv) <=> Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]]
Axiom
Define: Finite
A set is said to be finite if and only if there is no injective (1-to-1) function mapping n to s
2 ALL(s):[Set(s) => [Finite(s)
<=> ALL(f):[ALL(a):[a e n => f(a) e s] => ~Injective(f,n,s)]]]
Axiom
Define: Injective
Injective(f,a,b) means function f: a --> b is a injective, i.e. a 1-to-1 mapping from a to b
3 ALL(f):ALL(a):ALL(b):[Injective(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
Axiom
REQUIRED PROPERTIES OF N
************************
4 Set(n)
Axiom
5 1 e n
Axiom
Required properties of + on n
6 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
7 ALL(a):[a e n => [~a=1 => EXIST(b):[b e n & a=b+1]]]
Axiom
Required properties of < on n
8 ALL(a):ALL(b):[a e n & b e n => [~a=b => a<b | b<a]]
Axiom
9 ALL(a):ALL(b):[a e n & b e n => [a<b => EXIST(c):[c e n & a+c=b]]]
Axiom
Induction
10 ALL(a):[Set(a) & ALL(b):[b e a => b e n] => [1 e a & ALL(b):[b e a => b+1 e a] => ALL(b):[b e n => b e a]]]
Axiom
PREVIOUS RESULTS USED
*********************
Lemma 1 Proof
*******
Establish the existence a power function such that:
pow(x,1) = x
pow(x,2) = x*x
pow(x,3) = x*x*x
and so on.
11 ALL(s):[Set(s)
& ALL(a):ALL(b):[a e s & b e s => a*b e s]
=> EXIST(pow):[ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]]]
Axiom
Lemma 2 Proof
*******
For each x0 in h, establish the existence of function f: n --> h such that f(x)=pow(x0,x)
f(1) = x0
f(2) = x0*x0
f(3) = x0*x0*x0
and so on.
12 ALL(s):ALL(pow):[Set(s)
& ALL(a):ALL(b):[a e s & b e s => a*b e s]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]
=> ALL(a):[a e s => EXIST(f):[ALL(b):[b e n => f(b) e s]
& ALL(b):[b e n => f(b)=pow(a,b)]]]]
Axiom
Lemma 3 Proof
*******
The product of powers rule: pow(x,y) * pow(x,z) = pow(x,y+z)
Analogous to x^y * x^z = x^(y+z)
13 ALL(s):ALL(pow):[Set(s)
& ALL(a):ALL(b):[a e s & b e s => a*b e s]
& ALL(a):ALL(b):ALL(c):[a e s & b e s & c e s => a*b*c=a*(b*c)]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]
=> ALL(a):ALL(b):ALL(c):[a e s & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]]
Axiom
Lemma 4 Proof
*******
Elementary results from group theory.
14 ALL(g):ALL(e):ALL(inv):[Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
=> ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
& inv(e)=e
& ALL(a):[a e g => inv(inv(a))=a]]
Axiom
PROOF
*****
Suppose that (g,*) is a group with identity e and inverse operator inv
15 Group(g,e,inv)
Premise
Apply definition of Group
16 ALL(e):ALL(inv):[Group(g,e,inv) <=> Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]]
U Spec, 1
17 ALL(inv):[Group(g,e,inv) <=> Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]]
U Spec, 16
18 Group(g,e,inv) <=> Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
U Spec, 17
19 [Group(g,e,inv) => Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]]
& [Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e] => Group(g,e,inv)]
Iff-And, 18
20 Group(g,e,inv) => Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
Split, 19
21 Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e] => Group(g,e,inv)
Split, 19
22 Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
Detach, 20, 15
Splitting out each statement...
Define: g
23 Set(g)
Split, 22
Define: *
24 ALL(a):ALL(b):[a e g & b e g => a*b e g]
Split, 22
* is associative
25 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]
Split, 22
Define: e
26 e e g
Split, 22
e is the identity element
27 ALL(a):[a e g => a*e=a & e*a=a]
Split, 22
Define: inv
28 ALL(a):[a e g => inv(a) e g]
Split, 22
inv(x) is the inverse of x
29 ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
Split, 22
Apply Lemma 4
30 ALL(e):ALL(inv):[Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
=> ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
& inv(e)=e
& ALL(a):[a e g => inv(inv(a))=a]]
U Spec, 14
31 ALL(inv):[Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
=> ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
& inv(e)=e
& ALL(a):[a e g => inv(inv(a))=a]]
U Spec, 30
32 Set(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)]
& e e g
& ALL(a):[a e g => a*e=a & e*a=a]
& ALL(a):[a e g => inv(a) e g]
& ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]
=> ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
& inv(e)=e
& ALL(a):[a e g => inv(inv(a))=a]
U Spec, 31
33 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]
& ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
& inv(e)=e
& ALL(a):[a e g => inv(inv(a))=a]
Detach, 32, 22
34 ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]
Split, 33
35 ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]
Split, 33
36 inv(e)=e
Split, 33
Suppose h is a non-empty, finite subset of g
37 Set(h)
& EXIST(a):a e h
& Finite(h)
& ALL(a):[a e h => a e g]
Premise
Splitting this premise...
38 Set(h)
Split, 37
39 EXIST(a):a e h
Split, 37
40 Finite(h)
Split, 37
41 ALL(a):[a e h => a e g]
Split, 37
'=>'
Prove: Group(h,e,inv) => ALL(a):ALL(b):[aeh & beh => a*b e h
Suppose...
42 Group(h,e,inv)
Premise
Apply the definition Group
43 ALL(e):ALL(inv):[Group(h,e,inv) <=> Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]]
U Spec, 1
44 ALL(inv):[Group(h,e,inv) <=> Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]]
U Spec, 43
45 Group(h,e,inv) <=> Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]
U Spec, 44
46 [Group(h,e,inv) => Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]]
& [Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e] => Group(h,e,inv)]
Iff-And, 45
47 Group(h,e,inv) => Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]
Split, 46
48 Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e] => Group(h,e,inv)
Split, 46
49 Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]
Detach, 47, 42
50 Set(h)
Split, 49
51 ALL(a):ALL(b):[a e h & b e h => a*b e h]
Split, 49
As Required:
52 Group(h,e,inv)
=> ALL(a):ALL(b):[a e h & b e h => a*b e h]
4 Conclusion, 42
'<='
Prove: ALL(a):ALL(b):[a e h & b e h => a*b e h] => Group(h,e,inv)
Suppose...
53 ALL(a):ALL(b):[a e h & b e h => a*b e h]
Premise
Apply the definition of Group
54 ALL(e):ALL(inv):[Group(h,e,inv) <=> Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]]
U Spec, 1
55 ALL(inv):[Group(h,e,inv) <=> Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]]
U Spec, 54
56 Group(h,e,inv) <=> Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]
U Spec, 55
57 [Group(h,e,inv) => Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]]
& [Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e] => Group(h,e,inv)]
Iff-And, 56
58 Group(h,e,inv) => Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]
Split, 57
Sufficient: For Group(h,e,inv)
59 Set(h)
& ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e] => Group(h,e,inv)
Split, 57
Prove: ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
Suppose...
60 x e h & y e h & z e h
Premise
61 x e h
Split, 60
62 y e h
Split, 60
63 z e h
Split, 60
Apply associtativity of * on g
64 ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]
U Spec, 25
65 ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]
U Spec, 64
66 x e g & y e g & z e g => x*y*z=x*(y*z)
U Spec, 65
67 x e h => x e g
U Spec, 41
68 x e g
Detach, 67, 61
69 y e h => y e g
U Spec, 41
70 y e g
Detach, 69, 62
71 z e h => z e g
U Spec, 41
72 z e g
Detach, 71, 63
73 x e g & y e g
Join, 68, 70
74 x e g & y e g & z e g
Join, 73, 72
75 x*y*z=x*(y*z)
Detach, 66, 74
As Required:
76 ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
4 Conclusion, 60
Prove: ALL(a):[a e h => a*e=a & e*a=a]
Suppose...
77 x e h
Premise
Apply definition of e on g
78 x e g => x*e=x & e*x=x
U Spec, 27
79 x e h => x e g
U Spec, 41
80 x e g
Detach, 79, 77
81 x*e=x & e*x=x
Detach, 78, 80
As Required:
82 ALL(a):[a e h => a*e=a & e*a=a]
4 Conclusion, 77
Prove: ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]
Suppose...
83 x e h
Premise
Apply the definition of inv
84 x e g => x*inv(x)=e & inv(x)*x=e
U Spec, 29
85 x e h => x e g
U Spec, 41
86 x e g
Detach, 85, 83
87 x*inv(x)=e & inv(x)*x=e
Detach, 84, 86
As Required:
88 ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]
4 Conclusion, 83
Apply Lemma 1
89 Set(g)
& ALL(a):ALL(b):[a e g & b e g => a*b e g]
=> EXIST(pow):[ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]]
U Spec, 11
90 Set(g) & ALL(a):ALL(b):[a e g & b e g => a*b e g]
Join, 23, 24
91 EXIST(pow):[ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]]
Detach, 89, 90
92 ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]
E Spec, 91
Define: pow function
93 ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
Split, 92
94 ALL(a):[a e g => pow(a,1)=a]
Split, 92
95 ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]
Split, 92
96 Set(g) & ALL(a):ALL(b):[a e g & b e g => a*b e g]
Join, 23, 24
97 Set(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)]
Join, 96, 25
98 Set(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)]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
Join, 97, 93
99 Set(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)]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
Join, 98, 94
100 Set(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)]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]
Join, 99, 95
Apply Lemma 2
101 ALL(pow):[Set(g)
& ALL(a):ALL(b):[a e g & b e g => a*b e g]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]
=> ALL(a):[a e g => EXIST(f):[ALL(b):[b e n => f(b) e g]
& ALL(b):[b e n => f(b)=pow(a,b)]]]]
U Spec, 12
102 Set(g)
& ALL(a):ALL(b):[a e g & b e g => a*b e g]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]
=> ALL(a):[a e g => EXIST(f):[ALL(b):[b e n => f(b) e g]
& ALL(b):[b e n => f(b)=pow(a,b)]]]
U Spec, 101
103 Set(g) & ALL(a):ALL(b):[a e g & b e g => a*b e g]
Join, 23, 24
104 Set(g) & ALL(a):ALL(b):[a e g & b e g => a*b e g]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
Join, 103, 93
105 Set(g) & ALL(a):ALL(b):[a e g & b e g => a*b e g]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
Join, 104, 94
106 Set(g) & ALL(a):ALL(b):[a e g & b e g => a*b e g]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]
Join, 105, 95
107 ALL(a):[a e g => EXIST(f):[ALL(b):[b e n => f(b) e g]
& ALL(b):[b e n => f(b)=pow(a,b)]]]
Detach, 102, 106
Prove: ALL(a):[a e h => e e h & inv(a) e h]
Suppose...
108 x e h
Premise
Apply the definition of h
109 x e h => x e g
U Spec, 41
110 x e g
Detach, 109, 108
Apply previous result
111 x e g => EXIST(f):[ALL(b):[b e n => f(b) e g]
& ALL(b):[b e n => f(b)=pow(x,b)]]
U Spec, 107
112 EXIST(f):[ALL(b):[b e n => f(b) e g]
& ALL(b):[b e n => f(b)=pow(x,b)]]
Detach, 111, 110
113 ALL(b):[b e n => f(b) e g]
& ALL(b):[b e n => f(b)=pow(x,b)]
E Spec, 112
Define: f
114 ALL(b):[b e n => f(b) e g]
Split, 113
115 ALL(b):[b e n => f(b)=pow(x,b)]
Split, 113
116 Set(h) => [Finite(h)
<=> ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]]
U Spec, 2
117 Finite(h)
<=> ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]
Detach, 116, 38
118 [Finite(h) => ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]]
& [ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)] => Finite(h)]
Iff-And, 117
119 Finite(h) => ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]
Split, 118
120 ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)] => Finite(h)
Split, 118
121 ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]
Detach, 119, 40
122 ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)
U Spec, 121
Prove by induction that * is closed on h
Apply Subset Axiom
123 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & f(a) e h]]
Subset, 4
124 Set(p1) & ALL(a):[a e p1 <=> a e n & f(a) e h]
E Spec, 123
Define: p1
The subset of n on which f is closed
125 Set(p1)
Split, 124
126 ALL(a):[a e p1 <=> a e n & f(a) e h]
Split, 124
Apply induction axiom
127 Set(p1) & ALL(b):[b e p1 => b e n] => [1 e p1 & ALL(b):[b e p1 => b+1 e p1] => ALL(b):[b e n => b e p1]]
U Spec, 10
Prove that p1 is a subset of n
Suppose...
128 y e p1
Premise
Apply the definition p1
129 y e p1 <=> y e n & f(y) e h
U Spec, 126
130 [y e p1 => y e n & f(y) e h]
& [y e n & f(y) e h => y e p1]
Iff-And, 129
131 y e p1 => y e n & f(y) e h
Split, 130
132 y e n & f(y) e h => y e p1
Split, 130
133 y e n & f(y) e h
Detach, 131, 128
134 y e n
Split, 133
As Required:
135 ALL(b):[b e p1 => b e n]
4 Conclusion, 128
136 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 125, 135
Sufficient: ALL(b):[b e n => b e p1]
137 1 e p1 & ALL(b):[b e p1 => b+1 e p1] => ALL(b):[b e n => b e p1]
Detach, 127, 136
Base Case
*********
Prove: 1 e p1
Apply the definition of p1
138 1 e p1 <=> 1 e n & f(1) e h
U Spec, 126
139 [1 e p1 => 1 e n & f(1) e h]
& [1 e n & f(1) e h => 1 e p1]
Iff-And, 138
140 1 e p1 => 1 e n & f(1) e h
Split, 139
141 1 e n & f(1) e h => 1 e p1
Split, 139
Apply definition of f
142 1 e n => f(1)=pow(x,1)
U Spec, 115
143 f(1)=pow(x,1)
Detach, 142, 5
144 x e g => pow(x,1)=x
U Spec, 94
145 pow(x,1)=x
Detach, 144, 110
146 f(1)=x
Substitute, 143, 145
147 f(1) e h
Substitute, 146, 108
148 1 e n & f(1) e h
Join, 5, 147
As Required:
149 1 e p1
Detach, 141, 148
Inductive Step
**************
Prove: ALL(b):[b e p1 => b+1 e p1]
Suppose...
150 y e p1
Premise
Apply definition of p1
151 y e p1 <=> y e n & f(y) e h
U Spec, 126
152 [y e p1 => y e n & f(y) e h]
& [y e n & f(y) e h => y e p1]
Iff-And, 151
153 y e p1 => y e n & f(y) e h
Split, 152
154 y e n & f(y) e h => y e p1
Split, 152
155 y e n & f(y) e h
Detach, 153, 150
156 y e n
Split, 155
157 f(y) e h
Split, 155
Apply definition of f
158 y e n => f(y)=pow(x,y)
U Spec, 115
159 f(y)=pow(x,y)
Detach, 158, 156
160 pow(x,y) e h
Substitute, 159, 157
Apply definition of p1
161 y+1 e p1 <=> y+1 e n & f(y+1) e h
U Spec, 126
162 [y+1 e p1 => y+1 e n & f(y+1) e h]
& [y+1 e n & f(y+1) e h => y+1 e p1]
Iff-And, 161
163 y+1 e p1 => y+1 e n & f(y+1) e h
Split, 162
Sufficient:
164 y+1 e n & f(y+1) e h => y+1 e p1
Split, 162
Apply definition of + on n
165 ALL(b):[y e n & b e n => y+b e n]
U Spec, 6
166 y e n & 1 e n => y+1 e n
U Spec, 165
167 y e n & 1 e n
Join, 156, 5
168 y+1 e n
Detach, 166, 167
Apply definiton of f
169 y+1 e n => f(y+1)=pow(x,y+1)
U Spec, 115
170 f(y+1)=pow(x,y+1)
Detach, 169, 168
171 ALL(b):[x e g & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 95
172 x e g & y e n => pow(x,y+1)=pow(x,y)*x
U Spec, 171
173 x e g & y e n
Join, 110, 156
174 pow(x,y+1)=pow(x,y)*x
Detach, 172, 173
Apply definition of * on g
175 ALL(b):[pow(x,y) e h & b e h => pow(x,y)*b e h]
U Spec, 53
176 pow(x,y) e h & x e h => pow(x,y)*x e h
U Spec, 175
177 pow(x,y) e h & x e h
Join, 160, 108
178 pow(x,y)*x e h
Detach, 176, 177
179 pow(x,y+1) e h
Substitute, 174, 178
180 f(y+1) e h
Substitute, 170, 179
181 y+1 e n & f(y+1) e h
Join, 168, 180
182 y+1 e p1
Detach, 164, 181
As Required:
183 ALL(b):[b e p1 => b+1 e p1]
4 Conclusion, 150
Joining results from base case and inductive step...
184 1 e p1 & ALL(b):[b e p1 => b+1 e p1]
Join, 149, 183
By induction, we have...
185 ALL(b):[b e n => b e p1]
Detach, 137, 184
Prove: ALL(a):[a e n => f(a) e h]
Suppose...
186 y e n
Premise
Apply previous result
187 y e n => y e p1
U Spec, 185
188 y e p1
Detach, 187, 186
Apply definition of p1
189 y e p1 <=> y e n & f(y) e h
U Spec, 126
190 [y e p1 => y e n & f(y) e h]
& [y e n & f(y) e h => y e p1]
Iff-And, 189
191 y e p1 => y e n & f(y) e h
Split, 190
192 y e n & f(y) e h => y e p1
Split, 190
193 y e n & f(y) e h
Detach, 191, 188
194 y e n
Split, 193
195 f(y) e h
Split, 193
f is closed on h
As Required:
196 ALL(a):[a e n => f(a) e h]
4 Conclusion, 186
Since h is finite, we must have:
197 ~Injective(f,n,h)
Detach, 122, 196
Apply the definition of Injective
198 ALL(a):ALL(b):[Injective(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
U Spec, 3
199 ALL(b):[Injective(f,n,b) <=> ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]]
U Spec, 198
200 Injective(f,n,h) <=> ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]
U Spec, 199
201 [Injective(f,n,h) => ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]] => Injective(f,n,h)]
Iff-And, 200
202 Injective(f,n,h) => ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]
Split, 201
203 ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]] => Injective(f,n,h)
Split, 201
204 ~Injective(f,n,h) => ~ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]
Contra, 203
205 ~ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]
Detach, 204, 197
206 ~~EXIST(c):~ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]
Quant, 205
207 EXIST(c):~ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]
Rem DNeg, 206
208 EXIST(c):~~EXIST(d):~[c e n & d e n => [f(c)=f(d) => c=d]]
Quant, 207
209 EXIST(c):EXIST(d):~[c e n & d e n => [f(c)=f(d) => c=d]]
Rem DNeg, 208
210 EXIST(c):EXIST(d):~~[c e n & d e n & ~[f(c)=f(d) => c=d]]
Imply-And, 209
211 EXIST(c):EXIST(d):[c e n & d e n & ~[f(c)=f(d) => c=d]]
Rem DNeg, 210
212 EXIST(c):EXIST(d):[c e n & d e n & ~~[f(c)=f(d) & ~c=d]]
Imply-And, 211
213 EXIST(c):EXIST(d):[c e n & d e n & [f(c)=f(d) & ~c=d]]
Rem DNeg, 212
214 EXIST(d):[t e n & d e n & [f(t)=f(d) & ~t=d]]
E Spec, 213
215 t e n & u e n & [f(t)=f(u) & ~t=u]
E Spec, 214
Define: t, u
Where f(t) = f(u)
216 t e n
Split, 215
217 u e n
Split, 215
218 f(t)=f(u) & ~t=u
Split, 215
219 f(t)=f(u)
Split, 218
220 ~t=u
Split, 218
Apply definiton of < on n
221 ALL(b):[t e n & b e n => [~t=b => t<b | b<t]]
U Spec, 8
222 t e n & u e n => [~t=u => t<u | u<t]
U Spec, 221
223 t e n & u e n
Join, 216, 217
224 ~t=u => t<u | u<t
Detach, 222, 223
Two cases to consider
(In an informal proof at this point, you might we would say something hand-wavey like
"without loss of generality, let t < u." Or "by symmetry, we have...." Unfortunately,
such arguments are not allowed in formal proofs.)
225 t<u | u<t
Detach, 224, 220
Prove: ALL(a):ALL(b):[a e n & b e n
=> [f(a)=f(b) => [a<b => e e h & inv(x) e h]]]
(This sub-proof will be used to make the formal equilavent of a symmetry argument.)
Suppose...
226 v e n & w e n
Premise
227 v e n
Split, 226
228 w e n
Split, 226
Prove: f(v)=f(w) => [v<w => e e h & inv(x) e h
Suppose...
229 f(v)=f(w)
Premise
Prove: v<w => e e h & inv(x) e h
Suppose...
230 v<w
Premise
Apply definition of < on n
231 ALL(b):[v e n & b e n => [v<b => EXIST(c):[c e n & v+c=b]]]
U Spec, 9
232 v e n & w e n => [v<w => EXIST(c):[c e n & v+c=w]]
U Spec, 231
233 v<w => EXIST(c):[c e n & v+c=w]
Detach, 232, 226
234 EXIST(c):[c e n & v+c=w]
Detach, 233, 230
235 y e n & v+y=w
E Spec, 234
Define: y
The difference between v and w
236 y e n
Split, 235
237 v+y=w
Split, 235
238 f(v)=f(v+y)
Substitute, 237, 229
Apply definition of f
239 v e n => f(v)=pow(x,v)
U Spec, 115
240 f(v)=pow(x,v)
Detach, 239, 227
241 pow(x,v)=f(v+y)
Substitute, 240, 238
Apply definition of f
242 v+y e n => f(v+y)=pow(x,v+y)
U Spec, 115
243 ALL(b):[v e n & b e n => v+b e n]
U Spec, 6
244 v e n & y e n => v+y e n
U Spec, 243
245 v e n & y e n
Join, 227, 236
246 v+y e n
Detach, 244, 245
247 f(v+y)=pow(x,v+y)
Detach, 242, 246
248 pow(x,v)=pow(x,v+y)
Substitute, 247, 241
Establish equivalent of Product of Powers Rule for (g,*)
Apply Lemma 3
249 ALL(pow):[Set(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)]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]
=> ALL(a):ALL(b):ALL(c):[a e g & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]]
U Spec, 13
250 Set(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)]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]
=> ALL(a):ALL(b):ALL(c):[a e g & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]
U Spec, 249
251 Set(g) & ALL(a):ALL(b):[a e g & b e g => a*b e g]
Join, 23, 24
252 Set(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)]
Join, 251, 25
253 Set(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)]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
Join, 252, 93
254 Set(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)]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
Join, 253, 94
255 Set(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)]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]
& ALL(a):[a e g => pow(a,1)=a]
& ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]
Join, 254, 95
Product of Powers Rule
256 ALL(a):ALL(b):ALL(c):[a e g & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]
Detach, 250, 255
Apply Product of Powers Rule
257 ALL(b):ALL(c):[x e g & b e n & c e n => pow(x,b)*pow(x,c)=pow(x,b+c)]
U Spec, 256
258 ALL(c):[x e g & v e n & c e n => pow(x,v)*pow(x,c)=pow(x,v+c)]
U Spec, 257
259 x e g & v e n & y e n => pow(x,v)*pow(x,y)=pow(x,v+y)
U Spec, 258
260 x e g & v e n
Join, 110, 227
261 x e g & v e n & y e n
Join, 260, 236
262 pow(x,v)*pow(x,y)=pow(x,v+y)
Detach, 259, 261
263 pow(x,v)=pow(x,v)*pow(x,y)
Substitute, 262, 248
Apply previous result
264 ALL(b):[pow(x,v) e g & b e g => [pow(x,v)*b=pow(x,v) => b=e]]
U Spec, 34
265 pow(x,v) e g & pow(x,y) e g => [pow(x,v)*pow(x,y)=pow(x,v) => pow(x,y)=e]
U Spec, 264
266 ALL(b):[x e g & b e n => pow(x,b) e g]
U Spec, 93
267 x e g & v e n => pow(x,v) e g
U Spec, 266
268 x e g & v e n
Join, 110, 227
269 pow(x,v) e g
Detach, 267, 268
Apply definition of pow
270 x e g & y e n => pow(x,y) e g
U Spec, 266
271 x e g & y e n
Join, 110, 236
272 pow(x,y) e g
Detach, 270, 271
273 pow(x,v) e g & pow(x,y) e g
Join, 269, 272
274 pow(x,v)*pow(x,y)=pow(x,v) => pow(x,y)=e
Detach, 265, 273
275 pow(x,v)*pow(x,y)=pow(x,v)
Sym, 263
276 pow(x,y)=e
Detach, 274, 275
Apply previous result
277 y e n => f(y) e h
U Spec, 196
278 f(y) e h
Detach, 277, 236
279 y e n => f(y)=pow(x,y)
U Spec, 115
280 f(y)=pow(x,y)
Detach, 279, 236
281 pow(x,y) e h
Substitute, 280, 278
As Required:
282 e e h
Substitute, 276, 281
Apply definition of inv on g
283 x e g => inv(x) e g
U Spec, 28
284 inv(x) e g
Detach, 283, 110
Apply definition of inv
285 x e g => x*inv(x)=e & inv(x)*x=e
U Spec, 29
286 x*inv(x)=e & inv(x)*x=e
Detach, 285, 110
287 x*inv(x)=e
Split, 286
288 inv(x)*x=e
Split, 286
Two sub-cases to consider:
289 y=1 | ~y=1
Or Not
Sub-case 1
Prove: y=1 => inv(x) e h
Suppose...
290 y=1
Premise
291 pow(x,1)=e
Substitute, 290, 276
Apply definition of pow
292 x e g => pow(x,1)=x
U Spec, 94
293 pow(x,1)=x
Detach, 292, 110
294 x=e
Substitute, 293, 291
295 inv(x)=e
Substitute, 294, 36
296 inv(x) e h
Substitute, 295, 282
As Required:
297 y=1 => inv(x) e h
4 Conclusion, 290
Sub-case 2
Prove: ~y=1 => inv(x) e h
Suppose...
298 ~y=1
Premise
Apply property of + on n
299 y e n => [~y=1 => EXIST(b):[b e n & y=b+1]]
U Spec, 7
300 ~y=1 => EXIST(b):[b e n & y=b+1]
Detach, 299, 236
301 EXIST(b):[b e n & y=b+1]
Detach, 300, 298
302 z e n & y=z+1
E Spec, 301
Define: z
The predecessor of y
303 z e n
Split, 302
304 y=z+1
Split, 302
305 pow(x,z+1)=e
Substitute, 304, 276
Apply definition of pow
306 ALL(b):[x e g & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 95
307 x e g & z e n => pow(x,z+1)=pow(x,z)*x
U Spec, 306
308 x e g & z e n
Join, 110, 303
309 pow(x,z+1)=pow(x,z)*x
Detach, 307, 308
310 pow(x,z)*x=e
Substitute, 309, 305
Apply previous result
311 ALL(b):[pow(x,z) e g & b e g => [pow(x,z)*b=e => inv(pow(x,z))=b & inv(b)=pow(x,z)]]
U Spec, 35
312 pow(x,z) e g & x e g => [pow(x,z)*x=e => inv(pow(x,z))=x & inv(x)=pow(x,z)]
U Spec, 311
313 ALL(b):[x e g & b e n => pow(x,b) e g]
U Spec, 93
314 x e g & z e n => pow(x,z) e g
U Spec, 313
315 x e g & z e n
Join, 110, 303
316 pow(x,z) e g
Detach, 314, 315
317 pow(x,z) e g & x e g
Join, 316, 110
318 pow(x,z)*x=e => inv(pow(x,z))=x & inv(x)=pow(x,z)
Detach, 312, 317
319 inv(pow(x,z))=x & inv(x)=pow(x,z)
Detach, 318, 310
320 inv(pow(x,z))=x
Split, 319
321 inv(x)=pow(x,z)
Split, 319
322 z e n => f(z) e h
U Spec, 196
323 f(z) e h
Detach, 322, 303
Apply definition of f
324 z e n => f(z)=pow(x,z)
U Spec, 115
325 f(z)=pow(x,z)
Detach, 324, 303
326 pow(x,z) e h
Substitute, 325, 323
327 inv(x) e h
Substitute, 321, 326
As Required:
328 ~y=1 => inv(x) e h
4 Conclusion, 298
Joining results for Cases Rule...
329 [y=1 => inv(x) e h] & [~y=1 => inv(x) e h]
Join, 297, 328
330 inv(x) e h
Cases, 289, 329
331 e e h & inv(x) e h
Join, 282, 330
As Required:
332 v<w => e e h & inv(x) e h
4 Conclusion, 230
As Required:
333 f(v)=f(w) => [v<w => e e h & inv(x) e h]
4 Conclusion, 229
As Required:
334 ALL(a):ALL(b):[a e n & b e n
=> [f(a)=f(b) => [a<b => e e h & inv(x) e h]]]
4 Conclusion, 226
Prove: u<t => e e h & inv(x) e h
Suppose...
335 t<u
Premise
336 ALL(b):[t e n & b e n
=> [f(t)=f(b) => [t<b => e e h & inv(x) e h]]]
U Spec, 334
337 t e n & u e n
=> [f(t)=f(u) => [t<u => e e h & inv(x) e h]]
U Spec, 336
338 t e n & u e n
Join, 216, 217
339 f(t)=f(u) => [t<u => e e h & inv(x) e h]
Detach, 337, 338
340 t<u => e e h & inv(x) e h
Detach, 339, 219
341 e e h & inv(x) e h
Detach, 340, 335
As Required:
342 t<u => e e h & inv(x) e h
4 Conclusion, 335
Prove: u<t => e e h & inv(x) e h
Suppose...
343 u<t
Premise
344 ALL(b):[u e n & b e n
=> [f(u)=f(b) => [u<b => e e h & inv(x) e h]]]
U Spec, 334
345 u e n & t e n
=> [f(u)=f(t) => [u<t => e e h & inv(x) e h]]
U Spec, 344
346 u e n & t e n
Join, 217, 216
347 f(u)=f(t) => [u<t => e e h & inv(x) e h]
Detach, 345, 346
348 f(t)=f(u) => [u<t => e e h & inv(x) e h]
Sym, 347
349 u<t => e e h & inv(x) e h
Detach, 348, 219
350 e e h & inv(x) e h
Detach, 349, 343
As Required:
351 u<t => e e h & inv(x) e h
4 Conclusion, 343
352 [t<u => e e h & inv(x) e h]
& [u<t => e e h & inv(x) e h]
Join, 342, 351
By "symmetry"...
353 e e h & inv(x) e h
Cases, 225, 352
As Required:
354 ALL(a):[a e h => e e h & inv(a) e h]
4 Conclusion, 108
Apply definition of h
355 h0 e h
E Spec, 39
356 h0 e h => e e h & inv(h0) e h
U Spec, 354
357 e e h & inv(h0) e h
Detach, 356, 355
As Required:
358 e e h
Split, 357
359 inv(h0) e h
Split, 357
Prove: ALL(a):[a e h => inv(a) e h]
Suppose...
360 x e h
Premise
Apply previous result
361 x e h => e e h & inv(x) e h
U Spec, 354
362 e e h & inv(x) e h
Detach, 361, 360
363 e e h
Split, 362
364 inv(x) e h
Split, 362
As Required:
365 ALL(a):[a e h => inv(a) e h]
4 Conclusion, 360
Joining results...
366 Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]
Join, 38, 53
367 Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
Join, 366, 76
368 Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
Join, 367, 358
369 Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
Join, 368, 82
370 Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
Join, 369, 365
371 Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]
& ALL(a):ALL(b):ALL(c):[a e h & b e h & c e h => a*b*c=a*(b*c)]
& e e h
& ALL(a):[a e h => a*e=a & e*a=a]
& ALL(a):[a e h => inv(a) e h]
& ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e]
Join, 370, 88
372 Group(h,e,inv)
Detach, 59, 371
As Required:
373 ALL(a):ALL(b):[a e h & b e h => a*b e h]
=> Group(h,e,inv)
4 Conclusion, 53
Joining results for Iff-And Rule
374 [Group(h,e,inv)
=> ALL(a):ALL(b):[a e h & b e h => a*b e h]]
& [ALL(a):ALL(b):[a e h & b e h => a*b e h]
=> Group(h,e,inv)]
Join, 52, 373
375 Group(h,e,inv)
<=> ALL(a):ALL(b):[a e h & b e h => a*b e h]
Iff-And, 374
As Required:
376 ALL(h):[Set(h)
& EXIST(a):a e h
& Finite(h)
& ALL(a):[a e h => a e g]
=> [Group(h,e,inv)
<=> ALL(a):ALL(b):[a e h & b e h => a*b e h]]]
4 Conclusion, 37
As Required:
377 ALL(g):ALL(e):ALL(inv):[Group(g,e,inv)
=> ALL(h):[Set(h)
& EXIST(a):a e h
& Finite(h)
& ALL(a):[a e h => a e g]
=> [Group(h,e,inv)
<=> ALL(a):ALL(b):[a e h & b e h => a*b e h]]]]
4 Conclusion, 15