Step |
Hyp |
Ref |
Expression |
1 |
|
ghmplusg.p |
|- .+ = ( +g ` N ) |
2 |
|
eqid |
|- ( Base ` M ) = ( Base ` M ) |
3 |
|
eqid |
|- ( Base ` N ) = ( Base ` N ) |
4 |
|
eqid |
|- ( +g ` M ) = ( +g ` M ) |
5 |
|
ghmgrp1 |
|- ( G e. ( M GrpHom N ) -> M e. Grp ) |
6 |
5
|
3ad2ant3 |
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> M e. Grp ) |
7 |
|
ghmgrp2 |
|- ( G e. ( M GrpHom N ) -> N e. Grp ) |
8 |
7
|
3ad2ant3 |
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> N e. Grp ) |
9 |
3 1
|
grpcl |
|- ( ( N e. Grp /\ x e. ( Base ` N ) /\ y e. ( Base ` N ) ) -> ( x .+ y ) e. ( Base ` N ) ) |
10 |
9
|
3expb |
|- ( ( N e. Grp /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( x .+ y ) e. ( Base ` N ) ) |
11 |
8 10
|
sylan |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` N ) /\ y e. ( Base ` N ) ) ) -> ( x .+ y ) e. ( Base ` N ) ) |
12 |
2 3
|
ghmf |
|- ( F e. ( M GrpHom N ) -> F : ( Base ` M ) --> ( Base ` N ) ) |
13 |
12
|
3ad2ant2 |
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> F : ( Base ` M ) --> ( Base ` N ) ) |
14 |
2 3
|
ghmf |
|- ( G e. ( M GrpHom N ) -> G : ( Base ` M ) --> ( Base ` N ) ) |
15 |
14
|
3ad2ant3 |
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> G : ( Base ` M ) --> ( Base ` N ) ) |
16 |
|
fvexd |
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> ( Base ` M ) e. _V ) |
17 |
|
inidm |
|- ( ( Base ` M ) i^i ( Base ` M ) ) = ( Base ` M ) |
18 |
11 13 15 16 16 17
|
off |
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> ( F oF .+ G ) : ( Base ` M ) --> ( Base ` N ) ) |
19 |
2 4 1
|
ghmlin |
|- ( ( F e. ( M GrpHom N ) /\ x e. ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( F ` ( x ( +g ` M ) y ) ) = ( ( F ` x ) .+ ( F ` y ) ) ) |
20 |
19
|
3expb |
|- ( ( F e. ( M GrpHom N ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( F ` ( x ( +g ` M ) y ) ) = ( ( F ` x ) .+ ( F ` y ) ) ) |
21 |
20
|
3ad2antl2 |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( F ` ( x ( +g ` M ) y ) ) = ( ( F ` x ) .+ ( F ` y ) ) ) |
22 |
2 4 1
|
ghmlin |
|- ( ( G e. ( M GrpHom N ) /\ x e. ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( G ` ( x ( +g ` M ) y ) ) = ( ( G ` x ) .+ ( G ` y ) ) ) |
23 |
22
|
3expb |
|- ( ( G e. ( M GrpHom N ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( G ` ( x ( +g ` M ) y ) ) = ( ( G ` x ) .+ ( G ` y ) ) ) |
24 |
23
|
3ad2antl3 |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( G ` ( x ( +g ` M ) y ) ) = ( ( G ` x ) .+ ( G ` y ) ) ) |
25 |
21 24
|
oveq12d |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( ( F ` ( x ( +g ` M ) y ) ) .+ ( G ` ( x ( +g ` M ) y ) ) ) = ( ( ( F ` x ) .+ ( F ` y ) ) .+ ( ( G ` x ) .+ ( G ` y ) ) ) ) |
26 |
|
simpl1 |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> N e. Abel ) |
27 |
|
ablcmn |
|- ( N e. Abel -> N e. CMnd ) |
28 |
26 27
|
syl |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> N e. CMnd ) |
29 |
13
|
ffvelrnda |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ x e. ( Base ` M ) ) -> ( F ` x ) e. ( Base ` N ) ) |
30 |
29
|
adantrr |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( F ` x ) e. ( Base ` N ) ) |
31 |
13
|
ffvelrnda |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ y e. ( Base ` M ) ) -> ( F ` y ) e. ( Base ` N ) ) |
32 |
31
|
adantrl |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( F ` y ) e. ( Base ` N ) ) |
33 |
15
|
ffvelrnda |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ x e. ( Base ` M ) ) -> ( G ` x ) e. ( Base ` N ) ) |
34 |
33
|
adantrr |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( G ` x ) e. ( Base ` N ) ) |
35 |
15
|
ffvelrnda |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ y e. ( Base ` M ) ) -> ( G ` y ) e. ( Base ` N ) ) |
36 |
35
|
adantrl |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( G ` y ) e. ( Base ` N ) ) |
37 |
3 1
|
cmn4 |
|- ( ( N e. CMnd /\ ( ( F ` x ) e. ( Base ` N ) /\ ( F ` y ) e. ( Base ` N ) ) /\ ( ( G ` x ) e. ( Base ` N ) /\ ( G ` y ) e. ( Base ` N ) ) ) -> ( ( ( F ` x ) .+ ( F ` y ) ) .+ ( ( G ` x ) .+ ( G ` y ) ) ) = ( ( ( F ` x ) .+ ( G ` x ) ) .+ ( ( F ` y ) .+ ( G ` y ) ) ) ) |
38 |
28 30 32 34 36 37
|
syl122anc |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( ( ( F ` x ) .+ ( F ` y ) ) .+ ( ( G ` x ) .+ ( G ` y ) ) ) = ( ( ( F ` x ) .+ ( G ` x ) ) .+ ( ( F ` y ) .+ ( G ` y ) ) ) ) |
39 |
25 38
|
eqtrd |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( ( F ` ( x ( +g ` M ) y ) ) .+ ( G ` ( x ( +g ` M ) y ) ) ) = ( ( ( F ` x ) .+ ( G ` x ) ) .+ ( ( F ` y ) .+ ( G ` y ) ) ) ) |
40 |
13
|
ffnd |
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> F Fn ( Base ` M ) ) |
41 |
40
|
adantr |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> F Fn ( Base ` M ) ) |
42 |
15
|
ffnd |
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> G Fn ( Base ` M ) ) |
43 |
42
|
adantr |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> G Fn ( Base ` M ) ) |
44 |
|
fvexd |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( Base ` M ) e. _V ) |
45 |
2 4
|
grpcl |
|- ( ( M e. Grp /\ x e. ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( x ( +g ` M ) y ) e. ( Base ` M ) ) |
46 |
45
|
3expb |
|- ( ( M e. Grp /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( x ( +g ` M ) y ) e. ( Base ` M ) ) |
47 |
6 46
|
sylan |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( x ( +g ` M ) y ) e. ( Base ` M ) ) |
48 |
|
fnfvof |
|- ( ( ( F Fn ( Base ` M ) /\ G Fn ( Base ` M ) ) /\ ( ( Base ` M ) e. _V /\ ( x ( +g ` M ) y ) e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` ( x ( +g ` M ) y ) ) = ( ( F ` ( x ( +g ` M ) y ) ) .+ ( G ` ( x ( +g ` M ) y ) ) ) ) |
49 |
41 43 44 47 48
|
syl22anc |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` ( x ( +g ` M ) y ) ) = ( ( F ` ( x ( +g ` M ) y ) ) .+ ( G ` ( x ( +g ` M ) y ) ) ) ) |
50 |
|
simprl |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> x e. ( Base ` M ) ) |
51 |
|
fnfvof |
|- ( ( ( F Fn ( Base ` M ) /\ G Fn ( Base ` M ) ) /\ ( ( Base ` M ) e. _V /\ x e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` x ) = ( ( F ` x ) .+ ( G ` x ) ) ) |
52 |
41 43 44 50 51
|
syl22anc |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` x ) = ( ( F ` x ) .+ ( G ` x ) ) ) |
53 |
|
simprr |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> y e. ( Base ` M ) ) |
54 |
|
fnfvof |
|- ( ( ( F Fn ( Base ` M ) /\ G Fn ( Base ` M ) ) /\ ( ( Base ` M ) e. _V /\ y e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` y ) = ( ( F ` y ) .+ ( G ` y ) ) ) |
55 |
41 43 44 53 54
|
syl22anc |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` y ) = ( ( F ` y ) .+ ( G ` y ) ) ) |
56 |
52 55
|
oveq12d |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( ( ( F oF .+ G ) ` x ) .+ ( ( F oF .+ G ) ` y ) ) = ( ( ( F ` x ) .+ ( G ` x ) ) .+ ( ( F ` y ) .+ ( G ` y ) ) ) ) |
57 |
39 49 56
|
3eqtr4d |
|- ( ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) /\ ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` ( x ( +g ` M ) y ) ) = ( ( ( F oF .+ G ) ` x ) .+ ( ( F oF .+ G ) ` y ) ) ) |
58 |
2 3 4 1 6 8 18 57
|
isghmd |
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> ( F oF .+ G ) e. ( M GrpHom N ) ) |