Metamath Proof Explorer

Theorem ghmplusg

Description: The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypothesis ghmplusg.p 
|- .+ = ( +g ` N )
Assertion ghmplusg 
|- ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> ( F oF .+ G ) e. ( M GrpHom N ) )

Proof

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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ) )