An original proof by Dan Christensen
This proof was written with the aid of DC Proof 2.0. (Free download at http://www.dcproof.com )
Theorem 1
---------
For all pairs of groups (g1,add1) and (g2,add2), there exists a set of all those homomorphisms from
(g1,add1) to (g2,add2):
ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Group(g1,add1) & Group(g2,add2)
=> EXIST(homs):[Set(homs)
& ALL(f):[f e homs <=> Hom(f,g1,add1,g2,add2)]]]
Starting with sets g1 and g1, we use axioms of set theory (Cartesian product, power set and subset axioms) to construct the required sets.
Theorem 2
---------
For every group (g,add), there is an identity morphism from (g,add) to itself:
ALL(g):ALL(add):[Group(g,add)
=> EXIST(id):[ALL(a):[a e g => id(a)=a] & Hom(id,g,add,g,add)]]
From a previous result, we have that, for every set x, there exists an identity function on x. Starting from the set g then, there exists an identity function id defined on g. It is shown here that id is also a homomorphism on the group (g,add).
Axioms
------
Define: Group
Group(g,add) means (g,add) is a group
1 ALL(g):ALL(add):[Group(g,add)
<=> Set(g)
& ALL(a):ALL(b):[a e g & b e g => add(a,b) e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g => neg(a) e g]
& 0 e g
& ALL(a):[a e g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g => add(a,neg(a))=0 & add(neg(a),a)=0]]]
Axiom
Define: Class of groups
2 ALL(a):ALL(b):[(a,b) e groups <=> Group(a,b)]
Axiom
Define: Hom
Hom(f,g1,add1,g2,add2) means f is a homomorphism from group (g1,add1) to group (g2,add2)
3 ALL(f):ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Hom(f,g1,add1,g2,add2)
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]]
Axiom
Previous Result: On every set, there exist an identity function defined on that set.
4 ALL(s):[Set(s)
=> EXIST(f):[Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e s & b e s]
& ALL(a):[a e s => EXIST(b):[b e s & (a,b) e f]]
& ALL(a):ALL(b):ALL(c):[(a,b) e f & (a,c) e f => b=c]
& ALL(a):[a e s => f(a)=a]]]
Axiom
Prove: ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Group(g1,add1) & Group(g2,add2)
=> EXIST(homs):[Set(homs)
& ALL(f):[f e homs <=> Hom(f,g1,add1,g2,add2)]]]
Suppose...
5 Group(g1,add1) & Group(g2,add2)
Premise
6 Group(g1,add1)
Split, 5
7 Group(g2,add2)
Split, 5
Apply definition of Group
8 ALL(add):[Group(g1,add)
<=> Set(g1)
& ALL(a):ALL(b):[a e g1 & b e g1 => add(a,b) e g1]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g1 => neg(a) e g1]
& 0 e g1
& ALL(a):[a e g1 => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g1 => add(a,neg(a))=0 & add(neg(a),a)=0]]]
U Spec, 1
9 Group(g1,add1)
<=> Set(g1)
& ALL(a):ALL(b):[a e g1 & b e g1 => add1(a,b) e g1]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => add1(add1(a,b),c)=add1(a,add1(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g1 => neg(a) e g1]
& 0 e g1
& ALL(a):[a e g1 => add1(0,a)=a & add1(a,0)=a]
& ALL(a):[a e g1 => add1(a,neg(a))=0 & add1(neg(a),a)=0]]
U Spec, 8
10 [Group(g1,add1) => Set(g1)
& ALL(a):ALL(b):[a e g1 & b e g1 => add1(a,b) e g1]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => add1(add1(a,b),c)=add1(a,add1(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g1 => neg(a) e g1]
& 0 e g1
& ALL(a):[a e g1 => add1(0,a)=a & add1(a,0)=a]
& ALL(a):[a e g1 => add1(a,neg(a))=0 & add1(neg(a),a)=0]]]
& [Set(g1)
& ALL(a):ALL(b):[a e g1 & b e g1 => add1(a,b) e g1]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => add1(add1(a,b),c)=add1(a,add1(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g1 => neg(a) e g1]
& 0 e g1
& ALL(a):[a e g1 => add1(0,a)=a & add1(a,0)=a]
& ALL(a):[a e g1 => add1(a,neg(a))=0 & add1(neg(a),a)=0]] => Group(g1,add1)]
Iff-And, 9
11 Group(g1,add1) => Set(g1)
& ALL(a):ALL(b):[a e g1 & b e g1 => add1(a,b) e g1]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => add1(add1(a,b),c)=add1(a,add1(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g1 => neg(a) e g1]
& 0 e g1
& ALL(a):[a e g1 => add1(0,a)=a & add1(a,0)=a]
& ALL(a):[a e g1 => add1(a,neg(a))=0 & add1(neg(a),a)=0]]
Split, 10
12 Set(g1)
& ALL(a):ALL(b):[a e g1 & b e g1 => add1(a,b) e g1]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => add1(add1(a,b),c)=add1(a,add1(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g1 => neg(a) e g1]
& 0 e g1
& ALL(a):[a e g1 => add1(0,a)=a & add1(a,0)=a]
& ALL(a):[a e g1 => add1(a,neg(a))=0 & add1(neg(a),a)=0]] => Group(g1,add1)
Split, 10
13 Set(g1)
& ALL(a):ALL(b):[a e g1 & b e g1 => add1(a,b) e g1]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => add1(add1(a,b),c)=add1(a,add1(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g1 => neg(a) e g1]
& 0 e g1
& ALL(a):[a e g1 => add1(0,a)=a & add1(a,0)=a]
& ALL(a):[a e g1 => add1(a,neg(a))=0 & add1(neg(a),a)=0]]
Detach, 11, 6
14 Set(g1)
Split, 13
15 ALL(a):ALL(b):[a e g1 & b e g1 => add1(a,b) e g1]
Split, 13
16 ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => add1(add1(a,b),c)=add1(a,add1(b,c))]
Split, 13
17 EXIST(neg):EXIST(0):[ALL(a):[a e g1 => neg(a) e g1]
& 0 e g1
& ALL(a):[a e g1 => add1(0,a)=a & add1(a,0)=a]
& ALL(a):[a e g1 => add1(a,neg(a))=0 & add1(neg(a),a)=0]]
Split, 13
18 ALL(add):[Group(g2,add)
<=> Set(g2)
& ALL(a):ALL(b):[a e g2 & b e g2 => add(a,b) e g2]
& ALL(a):ALL(b):ALL(c):[a e g2 & b e g2 & c e g2 => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g2 => neg(a) e g2]
& 0 e g2
& ALL(a):[a e g2 => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g2 => add(a,neg(a))=0 & add(neg(a),a)=0]]]
U Spec, 1
19 Group(g2,add2)
<=> Set(g2)
& ALL(a):ALL(b):[a e g2 & b e g2 => add2(a,b) e g2]
& ALL(a):ALL(b):ALL(c):[a e g2 & b e g2 & c e g2 => add2(add2(a,b),c)=add2(a,add2(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g2 => neg(a) e g2]
& 0 e g2
& ALL(a):[a e g2 => add2(0,a)=a & add2(a,0)=a]
& ALL(a):[a e g2 => add2(a,neg(a))=0 & add2(neg(a),a)=0]]
U Spec, 18
20 [Group(g2,add2) => Set(g2)
& ALL(a):ALL(b):[a e g2 & b e g2 => add2(a,b) e g2]
& ALL(a):ALL(b):ALL(c):[a e g2 & b e g2 & c e g2 => add2(add2(a,b),c)=add2(a,add2(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g2 => neg(a) e g2]
& 0 e g2
& ALL(a):[a e g2 => add2(0,a)=a & add2(a,0)=a]
& ALL(a):[a e g2 => add2(a,neg(a))=0 & add2(neg(a),a)=0]]]
& [Set(g2)
& ALL(a):ALL(b):[a e g2 & b e g2 => add2(a,b) e g2]
& ALL(a):ALL(b):ALL(c):[a e g2 & b e g2 & c e g2 => add2(add2(a,b),c)=add2(a,add2(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g2 => neg(a) e g2]
& 0 e g2
& ALL(a):[a e g2 => add2(0,a)=a & add2(a,0)=a]
& ALL(a):[a e g2 => add2(a,neg(a))=0 & add2(neg(a),a)=0]] => Group(g2,add2)]
Iff-And, 19
21 Group(g2,add2) => Set(g2)
& ALL(a):ALL(b):[a e g2 & b e g2 => add2(a,b) e g2]
& ALL(a):ALL(b):ALL(c):[a e g2 & b e g2 & c e g2 => add2(add2(a,b),c)=add2(a,add2(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g2 => neg(a) e g2]
& 0 e g2
& ALL(a):[a e g2 => add2(0,a)=a & add2(a,0)=a]
& ALL(a):[a e g2 => add2(a,neg(a))=0 & add2(neg(a),a)=0]]
Split, 20
22 Set(g2)
& ALL(a):ALL(b):[a e g2 & b e g2 => add2(a,b) e g2]
& ALL(a):ALL(b):ALL(c):[a e g2 & b e g2 & c e g2 => add2(add2(a,b),c)=add2(a,add2(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g2 => neg(a) e g2]
& 0 e g2
& ALL(a):[a e g2 => add2(0,a)=a & add2(a,0)=a]
& ALL(a):[a e g2 => add2(a,neg(a))=0 & add2(neg(a),a)=0]] => Group(g2,add2)
Split, 20
23 Set(g2)
& ALL(a):ALL(b):[a e g2 & b e g2 => add2(a,b) e g2]
& ALL(a):ALL(b):ALL(c):[a e g2 & b e g2 & c e g2 => add2(add2(a,b),c)=add2(a,add2(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g2 => neg(a) e g2]
& 0 e g2
& ALL(a):[a e g2 => add2(0,a)=a & add2(a,0)=a]
& ALL(a):[a e g2 => add2(a,neg(a))=0 & add2(neg(a),a)=0]]
Detach, 21, 7
24 Set(g2)
Split, 23
25 ALL(a):ALL(b):[a e g2 & b e g2 => add2(a,b) e g2]
Split, 23
26 ALL(a):ALL(b):ALL(c):[a e g2 & b e g2 & c e g2 => add2(add2(a,b),c)=add2(a,add2(b,c))]
Split, 23
27 EXIST(neg):EXIST(0):[ALL(a):[a e g2 => neg(a) e g2]
& 0 e g2
& ALL(a):[a e g2 => add2(0,a)=a & add2(a,0)=a]
& ALL(a):[a e g2 => add2(a,neg(a))=0 & add2(neg(a),a)=0]]
Split, 23
Construct the Cartesian product of g1 and g2
28 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
29 ALL(a2):[Set(g1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e g1 & c2 e a2]]]
U Spec, 28
30 Set(g1) & Set(g2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e g1 & c2 e g2]]
U Spec, 29
31 Set(g1) & Set(g2)
Join, 14, 24
32 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e g1 & c2 e g2]]
Detach, 30, 31
33 Set'(g1xg2) & ALL(c1):ALL(c2):[(c1,c2) e g1xg2 <=> c1 e g1 & c2 e g2]
E Spec, 32
Define: g1xg2
34 Set'(g1xg2)
Split, 33
35 ALL(c1):ALL(c2):[(c1,c2) e g1xg2 <=> c1 e g1 & c2 e g2]
Split, 33
Construct the power set of g1 x g2
36 ALL(a):[Set'(a) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e a]]]]
Power Set
37 Set'(g1xg2) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e g1xg2]]]
U Spec, 36
38 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e g1xg2]]]
Detach, 37, 34
39 Set(pg1xg2)
& ALL(c):[c e pg1xg2 <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e g1xg2]]
E Spec, 38
Define: pg1xg2 (the power set of g1xg2)
40 Set(pg1xg2)
Split, 39
41 ALL(c):[c e pg1xg2 <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e g1xg2]]
Split, 39
Construct the set of all functions mapping g1 to g2
42 EXIST(sub):[Set(sub) & ALL(f):[f e sub <=> f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]]]
Subset, 40
43 Set(fg1g2) & ALL(f):[f e fg1g2 <=> f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]]
E Spec, 42
Define: fg1g2 (the set of all functions mapping g1 to g2)
44 Set(fg1g2)
Split, 43
45 ALL(f):[f e fg1g2 <=> f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]]
Split, 43
Construct the set of homomorphisms from group (g1,add1) to (g2,add2)
46 EXIST(sub):[Set(sub) & ALL(f):[f e sub <=> f e fg1g2 & Hom(f,g1,add1,g2,add2)]]
Subset, 44
47 Set(homs) & ALL(f):[f e homs <=> f e fg1g2 & Hom(f,g1,add1,g2,add2)]
E Spec, 46
Define: homs (the set of homomorphisms from group (g1,add1) to (g2,add2))
48 Set(homs)
Split, 47
49 ALL(f):[f e homs <=> f e fg1g2 & Hom(f,g1,add1,g2,add2)]
Split, 47
Prove: ALL(f):[f e fg1g2
=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
Suppose...
50 f e fg1g2
Premise
Apply definition of fg1g2
51 f e fg1g2 <=> f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
U Spec, 45
52 [f e fg1g2 => f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]]
& [f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]] => f e fg1g2]
Iff-And, 51
53 f e fg1g2 => f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
Split, 52
54 f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]] => f e fg1g2
Split, 52
55 f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
Detach, 53, 50
56 f e pg1xg2
Split, 55
57 ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Split, 55
58 ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
Split, 57
59 ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
Split, 57
60 ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Split, 57
Apply definition of pg1xg2
61 f e pg1xg2 <=> Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2]
U Spec, 41
62 [f e pg1xg2 => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2]]
& [Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2] => f e pg1xg2]
Iff-And, 61
63 f e pg1xg2 => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2]
Split, 62
64 Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2] => f e pg1xg2
Split, 62
65 Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2]
Detach, 63, 56
66 Set'(f)
Split, 65
67 ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2]
Split, 65
68 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
Join, 66, 58
69 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
Join, 68, 59
70 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Join, 69, 60
As Required:
71 ALL(f):[f e fg1g2
=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
4 Conclusion, 50
Prove: ALL(f):[Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
=> f e fg1g2]
Suppose...
72 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Premise
73 Set'(f)
Split, 72
74 ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
Split, 72
75 ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
Split, 72
76 ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Split, 72
Apply definition of fg1g2
77 f e fg1g2 <=> f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
U Spec, 45
78 [f e fg1g2 => f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]]
& [f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]] => f e fg1g2]
Iff-And, 77
79 f e fg1g2 => f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
Split, 78
Sufficient: For f e fg1g2
80 f e pg1xg2 & [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]] => f e fg1g2
Split, 78
Apply definition of pg1xg2
81 f e pg1xg2 <=> Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2]
U Spec, 41
82 [f e pg1xg2 => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2]]
& [Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2] => f e pg1xg2]
Iff-And, 81
83 f e pg1xg2 => Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2]
Split, 82
Sufficient: For f e pg1xg2
84 Set'(f) & ALL(d1):ALL(d2):[(d1,d2) e f => (d1,d2) e g1xg2] => f e pg1xg2
Split, 82
Prove: ALL(a):ALL(b):[(a,b) e f => (a,b) e g1xg2]
Suppose...
85 (p,q) e f
Premise
Apply definition of f
86 ALL(b):[(p,b) e f => p e g1 & b e g2]
U Spec, 74
87 (p,q) e f => p e g1 & q e g2
U Spec, 86
88 p e g1 & q e g2
Detach, 87, 85
Apply definiton of g1xg2
89 ALL(c2):[(p,c2) e g1xg2 <=> p e g1 & c2 e g2]
U Spec, 35
90 (p,q) e g1xg2 <=> p e g1 & q e g2
U Spec, 89
91 [(p,q) e g1xg2 => p e g1 & q e g2]
& [p e g1 & q e g2 => (p,q) e g1xg2]
Iff-And, 90
92 (p,q) e g1xg2 => p e g1 & q e g2
Split, 91
93 p e g1 & q e g2 => (p,q) e g1xg2
Split, 91
94 (p,q) e g1xg2
Detach, 93, 88
As Required:
95 ALL(a):ALL(b):[(a,b) e f => (a,b) e g1xg2]
4 Conclusion, 85
96 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => (a,b) e g1xg2]
Join, 73, 95
97 f e pg1xg2
Detach, 84, 96
98 ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
Join, 74, 75
99 ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Join, 98, 76
100 f e pg1xg2
& [ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
Join, 97, 99
101 f e fg1g2
Detach, 80, 100
As Required:
102 ALL(f):[Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
=> f e fg1g2]
4 Conclusion, 72
103 ALL(f):[[f e fg1g2
=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]] & [Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
=> f e fg1g2]]
Join, 71, 102
As Required:
104 ALL(f):[f e fg1g2
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
Iff-And, 103
105 f e homs
Premise
106 f e homs <=> f e fg1g2 & Hom(f,g1,add1,g2,add2)
U Spec, 49
107 [f e homs => f e fg1g2 & Hom(f,g1,add1,g2,add2)]
& [f e fg1g2 & Hom(f,g1,add1,g2,add2) => f e homs]
Iff-And, 106
108 f e homs => f e fg1g2 & Hom(f,g1,add1,g2,add2)
Split, 107
109 f e fg1g2 & Hom(f,g1,add1,g2,add2) => f e homs
Split, 107
110 f e fg1g2 & Hom(f,g1,add1,g2,add2)
Detach, 108, 105
111 f e fg1g2
Split, 110
112 Hom(f,g1,add1,g2,add2)
Split, 110
As Required:
113 ALL(f):[f e homs => Hom(f,g1,add1,g2,add2)]
4 Conclusion, 105
Suppose...
114 Hom(f,g1,add1,g2,add2)
Premise
115 f e homs <=> f e fg1g2 & Hom(f,g1,add1,g2,add2)
U Spec, 49
116 [f e homs => f e fg1g2 & Hom(f,g1,add1,g2,add2)]
& [f e fg1g2 & Hom(f,g1,add1,g2,add2) => f e homs]
Iff-And, 115
117 f e homs => f e fg1g2 & Hom(f,g1,add1,g2,add2)
Split, 116
Sufficient: For f e homs
118 f e fg1g2 & Hom(f,g1,add1,g2,add2) => f e homs
Split, 116
Apply definition of Hom
119 ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Hom(f,g1,add1,g2,add2)
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]]
U Spec, 3
120 ALL(add1):ALL(g2):ALL(add2):[Hom(f,g1,add1,g2,add2)
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]]
U Spec, 119
121 ALL(g2):ALL(add2):[Hom(f,g1,add1,g2,add2)
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]]
U Spec, 120
122 ALL(add2):[Hom(f,g1,add1,g2,add2)
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]]
U Spec, 121
123 Hom(f,g1,add1,g2,add2)
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]
U Spec, 122
124 [Hom(f,g1,add1,g2,add2) => Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]]
& [Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]] => Hom(f,g1,add1,g2,add2)]
Iff-And, 123
125 Hom(f,g1,add1,g2,add2) => Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]
Split, 124
126 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]] => Hom(f,g1,add1,g2,add2)
Split, 124
127 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]
Detach, 125, 114
128 Set'(f)
Split, 127
129 ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
Split, 127
130 ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
Split, 127
131 ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Split, 127
132 ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(f(a),f(b))=f(c)]]
Split, 127
Apply definition of fg1g2
133 f e fg1g2
<=> Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
U Spec, 104
134 [f e fg1g2 => Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
& [Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2] => f e fg1g2]
Iff-And, 133
135 f e fg1g2 => Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Split, 134
Sufficient: For f e fg1g2
136 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2] => f e fg1g2
Split, 134
137 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
Join, 128, 129
138 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
Join, 137, 130
139 Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Join, 138, 131
140 f e fg1g2
Detach, 136, 139
141 f e fg1g2 & Hom(f,g1,add1,g2,add2)
Join, 140, 114
142 f e homs
Detach, 118, 141
As Required:
143 ALL(f):[Hom(f,g1,add1,g2,add2) => f e homs]
4 Conclusion, 114
144 ALL(f):[[f e homs => Hom(f,g1,add1,g2,add2)] & [Hom(f,g1,add1,g2,add2) => f e homs]]
Join, 113, 143
145 ALL(f):[f e homs <=> Hom(f,g1,add1,g2,add2)]
Iff-And, 144
Theorem 1
---------
As Required:
146 ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Group(g1,add1) & Group(g2,add2)
=> EXIST(homs):ALL(f):[f e homs <=> Hom(f,g1,add1,g2,add2)]]
4 Conclusion, 5
Prove: ALL(g):ALL(add):[Group(g,add) => EXIST(id):Hom(id,g,add,g,add)]
Suppose...
147 Group(g,add)
Premise
Apply Theorem 1
148 ALL(add1):ALL(g2):ALL(add2):[Group(g,add1) & Group(g2,add2)
=> EXIST(homs):ALL(f):[f e homs <=> Hom(f,g,add1,g2,add2)]]
U Spec, 146
149 ALL(g2):ALL(add2):[Group(g,add) & Group(g2,add2)
=> EXIST(homs):ALL(f):[f e homs <=> Hom(f,g,add,g2,add2)]]
U Spec, 148
150 ALL(add2):[Group(g,add) & Group(g,add2)
=> EXIST(homs):ALL(f):[f e homs <=> Hom(f,g,add,g,add2)]]
U Spec, 149
151 Group(g,add) & Group(g,add)
=> EXIST(homs):ALL(f):[f e homs <=> Hom(f,g,add,g,add)]
U Spec, 150
152 Group(g,add) & Group(g,add)
Join, 147, 147
153 EXIST(homs):ALL(f):[f e homs <=> Hom(f,g,add,g,add)]
Detach, 151, 152
154 ALL(f):[f e idhoms <=> Hom(f,g,add,g,add)]
E Spec, 153
Apply definition of Group
155 ALL(add):[Group(g,add)
<=> Set(g)
& ALL(a):ALL(b):[a e g & b e g => add(a,b) e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g => neg(a) e g]
& 0 e g
& ALL(a):[a e g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g => add(a,neg(a))=0 & add(neg(a),a)=0]]]
U Spec, 1
156 Group(g,add)
<=> Set(g)
& ALL(a):ALL(b):[a e g & b e g => add(a,b) e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g => neg(a) e g]
& 0 e g
& ALL(a):[a e g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g => add(a,neg(a))=0 & add(neg(a),a)=0]]
U Spec, 155
157 [Group(g,add) => Set(g)
& ALL(a):ALL(b):[a e g & b e g => add(a,b) e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g => neg(a) e g]
& 0 e g
& ALL(a):[a e g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g => add(a,neg(a))=0 & add(neg(a),a)=0]]]
& [Set(g)
& ALL(a):ALL(b):[a e g & b e g => add(a,b) e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g => neg(a) e g]
& 0 e g
& ALL(a):[a e g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g => add(a,neg(a))=0 & add(neg(a),a)=0]] => Group(g,add)]
Iff-And, 156
158 Group(g,add) => Set(g)
& ALL(a):ALL(b):[a e g & b e g => add(a,b) e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g => neg(a) e g]
& 0 e g
& ALL(a):[a e g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g => add(a,neg(a))=0 & add(neg(a),a)=0]]
Split, 157
159 Set(g)
& ALL(a):ALL(b):[a e g & b e g => add(a,b) e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g => neg(a) e g]
& 0 e g
& ALL(a):[a e g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g => add(a,neg(a))=0 & add(neg(a),a)=0]] => Group(g,add)
Split, 157
160 Set(g)
& ALL(a):ALL(b):[a e g & b e g => add(a,b) e g]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => add(add(a,b),c)=add(a,add(b,c))]
& EXIST(neg):EXIST(0):[ALL(a):[a e g => neg(a) e g]
& 0 e g
& ALL(a):[a e g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g => add(a,neg(a))=0 & add(neg(a),a)=0]]
Detach, 158, 147
161 Set(g)
Split, 160
162 ALL(a):ALL(b):[a e g & b e g => add(a,b) e g]
Split, 160
163 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => add(add(a,b),c)=add(a,add(b,c))]
Split, 160
164 EXIST(neg):EXIST(0):[ALL(a):[a e g => neg(a) e g]
& 0 e g
& ALL(a):[a e g => add(0,a)=a & add(a,0)=a]
& ALL(a):[a e g => add(a,neg(a))=0 & add(neg(a),a)=0]]
Split, 160
Apply previous result
165 Set(g)
=> EXIST(f):[Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e f]]
& ALL(a):ALL(b):ALL(c):[(a,b) e f & (a,c) e f => b=c]
& ALL(a):[a e g => f(a)=a]]
U Spec, 4
166 EXIST(f):[Set'(f)
& ALL(a):ALL(b):[(a,b) e f => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e f]]
& ALL(a):ALL(b):ALL(c):[(a,b) e f & (a,c) e f => b=c]
& ALL(a):[a e g => f(a)=a]]
Detach, 165, 161
167 Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
& ALL(a):ALL(b):ALL(c):[(a,b) e id & (a,c) e id => b=c]
& ALL(a):[a e g => id(a)=a]
E Spec, 166
Define: id
168 Set'(id)
Split, 167
169 ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
Split, 167
170 ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
Split, 167
171 ALL(a):ALL(b):ALL(c):[(a,b) e id & (a,c) e id => b=c]
Split, 167
172 ALL(a):[a e g => id(a)=a]
Split, 167
Apply previous result
173 id e idhoms <=> Hom(id,g,add,g,add)
U Spec, 154
174 [id e idhoms => Hom(id,g,add,g,add)]
& [Hom(id,g,add,g,add) => id e idhoms]
Iff-And, 173
175 id e idhoms => Hom(id,g,add,g,add)
Split, 174
Sufficient: For id e idhoms
176 Hom(id,g,add,g,add) => id e idhoms
Split, 174
Apply definition of Hom
177 ALL(g1):ALL(add1):ALL(g2):ALL(add2):[Hom(id,g1,add1,g2,add2)
<=> Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g1 & b e g2]
& ALL(a):[a e g1 => EXIST(b):[b e g2 & (a,b) e id]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e id & (a,b2) e id => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g1 & b e g1 & c e g1 => [add1(a,b)=c => add2(id(a),id(b))=id(c)]]]
U Spec, 3
178 ALL(add1):ALL(g2):ALL(add2):[Hom(id,g,add1,g2,add2)
<=> Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g2]
& ALL(a):[a e g => EXIST(b):[b e g2 & (a,b) e id]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e id & (a,b2) e id => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [add1(a,b)=c => add2(id(a),id(b))=id(c)]]]
U Spec, 177
179 ALL(g2):ALL(add2):[Hom(id,g,add,g2,add2)
<=> Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g2]
& ALL(a):[a e g => EXIST(b):[b e g2 & (a,b) e id]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e id & (a,b2) e id => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [add(a,b)=c => add2(id(a),id(b))=id(c)]]]
U Spec, 178
180 ALL(add2):[Hom(id,g,add,g,add2)
<=> Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e id & (a,b2) e id => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [add(a,b)=c => add2(id(a),id(b))=id(c)]]]
U Spec, 179
181 Hom(id,g,add,g,add)
<=> Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e id & (a,b2) e id => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [add(a,b)=c => add(id(a),id(b))=id(c)]]
U Spec, 180
182 [Hom(id,g,add,g,add) => Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e id & (a,b2) e id => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [add(a,b)=c => add(id(a),id(b))=id(c)]]]
& [Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e id & (a,b2) e id => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [add(a,b)=c => add(id(a),id(b))=id(c)]] => Hom(id,g,add,g,add)]
Iff-And, 181
183 Hom(id,g,add,g,add) => Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e id & (a,b2) e id => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [add(a,b)=c => add(id(a),id(b))=id(c)]]
Split, 182
Sufficient: For Hom(id,g,add,g,add)
184 Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e id & (a,b2) e id => b1=b2]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [add(a,b)=c => add(id(a),id(b))=id(c)]] => Hom(id,g,add,g,add)
Split, 182
Prove: ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g
=> [add(a,b)=c => add(id(a),id(b))=id(c)]]
Suppose...
185 x e g & y e g & z e g
Premise
186 x e g
Split, 185
187 y e g
Split, 185
188 z e g
Split, 185
Prove: add(x,y)=z => add(id(x),id(y))=id(z)
Suppose...
189 add(x,y)=z
Premise
Apply definition of id
190 x e g => id(x)=x
U Spec, 172
191 id(x)=x
Detach, 190, 186
192 y e g => id(y)=y
U Spec, 172
193 id(y)=y
Detach, 192, 187
194 z e g => id(z)=z
U Spec, 172
195 id(z)=z
Detach, 194, 188
196 add(id(x),y)=z
Substitute, 191, 189
197 add(id(x),id(y))=z
Substitute, 193, 196
198 add(id(x),id(y))=id(z)
Substitute, 195, 197
As Required:
199 add(x,y)=z => add(id(x),id(y))=id(z)
4 Conclusion, 189
As Required:
200 ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g
=> [add(a,b)=c => add(id(a),id(b))=id(c)]]
4 Conclusion, 185
201 Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
Join, 168, 169
202 Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
Join, 201, 170
203 Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
& ALL(a):ALL(b):ALL(c):[(a,b) e id & (a,c) e id => b=c]
Join, 202, 171
204 Set'(id)
& ALL(a):ALL(b):[(a,b) e id => a e g & b e g]
& ALL(a):[a e g => EXIST(b):[b e g & (a,b) e id]]
& ALL(a):ALL(b):ALL(c):[(a,b) e id & (a,c) e id => b=c]
& ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g
=> [add(a,b)=c => add(id(a),id(b))=id(c)]]
Join, 203, 200
205 Hom(id,g,add,g,add)
Detach, 184, 204
Theorem 2
---------
As Required:
206 ALL(g):ALL(add):[Group(g,add) => EXIST(id):Hom(id,g,add,g,add)]
4 Conclusion, 147