Metamath Proof Explorer

Theorem lmhmplusg

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

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

Proof

Step Hyp Ref Expression
1 lmhmplusg.p 
 |-  .+ = ( +g ` N )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( .s ` M ) = ( .s ` M )
4 eqid 
 |-  ( .s ` N ) = ( .s ` N )
5 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
6 eqid 
 |-  ( Scalar ` N ) = ( Scalar ` N )
7 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
8 lmhmlmod1 
 |-  ( F e. ( M LMHom N ) -> M e. LMod )
9 8 adantr 
 |-  ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) -> M e. LMod )
10 lmhmlmod2 
 |-  ( F e. ( M LMHom N ) -> N e. LMod )
11 10 adantr 
 |-  ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) -> N e. LMod )
12 5 6 lmhmsca 
 |-  ( F e. ( M LMHom N ) -> ( Scalar ` N ) = ( Scalar ` M ) )
13 12 adantr 
 |-  ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) -> ( Scalar ` N ) = ( Scalar ` M ) )
14 lmodabl 
 |-  ( N e. LMod -> N e. Abel )
15 11 14 syl 
 |-  ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) -> N e. Abel )
16 lmghm 
 |-  ( F e. ( M LMHom N ) -> F e. ( M GrpHom N ) )
17 16 adantr 
 |-  ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) -> F e. ( M GrpHom N ) )
18 lmghm 
 |-  ( G e. ( M LMHom N ) -> G e. ( M GrpHom N ) )
19 18 adantl 
 |-  ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) -> G e. ( M GrpHom N ) )
20 1 ghmplusg 
 |-  ( ( N e. Abel /\ F e. ( M GrpHom N ) /\ G e. ( M GrpHom N ) ) -> ( F oF .+ G ) e. ( M GrpHom N ) )
21 15 17 19 20 syl3anc 
 |-  ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) -> ( F oF .+ G ) e. ( M GrpHom N ) )
22 simpll 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> F e. ( M LMHom N ) )
23 simprl 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> x e. ( Base ` ( Scalar ` M ) ) )
24 simprr 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> y e. ( Base ` M ) )
25 5 7 2 3 4 lmhmlin 
 |-  ( ( F e. ( M LMHom N ) /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) -> ( F ` ( x ( .s ` M ) y ) ) = ( x ( .s ` N ) ( F ` y ) ) )
26 22 23 24 25 syl3anc 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( F ` ( x ( .s ` M ) y ) ) = ( x ( .s ` N ) ( F ` y ) ) )
27 simplr 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> G e. ( M LMHom N ) )
28 5 7 2 3 4 lmhmlin 
 |-  ( ( G e. ( M LMHom N ) /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) -> ( G ` ( x ( .s ` M ) y ) ) = ( x ( .s ` N ) ( G ` y ) ) )
29 27 23 24 28 syl3anc 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( G ` ( x ( .s ` M ) y ) ) = ( x ( .s ` N ) ( G ` y ) ) )
30 26 29 oveq12d 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( ( F ` ( x ( .s ` M ) y ) ) .+ ( G ` ( x ( .s ` M ) y ) ) ) = ( ( x ( .s ` N ) ( F ` y ) ) .+ ( x ( .s ` N ) ( G ` y ) ) ) )
31 10 ad2antrr 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> N e. LMod )
32 12 fveq2d 
 |-  ( F e. ( M LMHom N ) -> ( Base ` ( Scalar ` N ) ) = ( Base ` ( Scalar ` M ) ) )
33 32 ad2antrr 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( Base ` ( Scalar ` N ) ) = ( Base ` ( Scalar ` M ) ) )
34 23 33 eleqtrrd 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> x e. ( Base ` ( Scalar ` N ) ) )
35 eqid 
 |-  ( Base ` N ) = ( Base ` N )
36 2 35 lmhmf 
 |-  ( F e. ( M LMHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
37 36 ad2antrr 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> F : ( Base ` M ) --> ( Base ` N ) )
38 37 24 ffvelrnd 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( F ` y ) e. ( Base ` N ) )
39 2 35 lmhmf 
 |-  ( G e. ( M LMHom N ) -> G : ( Base ` M ) --> ( Base ` N ) )
40 39 ad2antlr 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> G : ( Base ` M ) --> ( Base ` N ) )
41 40 24 ffvelrnd 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( G ` y ) e. ( Base ` N ) )
42 eqid 
 |-  ( Base ` ( Scalar ` N ) ) = ( Base ` ( Scalar ` N ) )
43 35 1 6 4 42 lmodvsdi 
 |-  ( ( N e. LMod /\ ( x e. ( Base ` ( Scalar ` N ) ) /\ ( F ` y ) e. ( Base ` N ) /\ ( G ` y ) e. ( Base ` N ) ) ) -> ( x ( .s ` N ) ( ( F ` y ) .+ ( G ` y ) ) ) = ( ( x ( .s ` N ) ( F ` y ) ) .+ ( x ( .s ` N ) ( G ` y ) ) ) )
44 31 34 38 41 43 syl13anc 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( x ( .s ` N ) ( ( F ` y ) .+ ( G ` y ) ) ) = ( ( x ( .s ` N ) ( F ` y ) ) .+ ( x ( .s ` N ) ( G ` y ) ) ) )
45 30 44 eqtr4d 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( ( F ` ( x ( .s ` M ) y ) ) .+ ( G ` ( x ( .s ` M ) y ) ) ) = ( x ( .s ` N ) ( ( F ` y ) .+ ( G ` y ) ) ) )
46 37 ffnd 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> F Fn ( Base ` M ) )
47 40 ffnd 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> G Fn ( Base ` M ) )
48 fvexd 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( Base ` M ) e. _V )
49 8 ad2antrr 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> M e. LMod )
50 2 5 3 7 lmodvscl 
 |-  ( ( M e. LMod /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) -> ( x ( .s ` M ) y ) e. ( Base ` M ) )
51 49 23 24 50 syl3anc 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( x ( .s ` M ) y ) e. ( Base ` M ) )
52 fnfvof 
 |-  ( ( ( F Fn ( Base ` M ) /\ G Fn ( Base ` M ) ) /\ ( ( Base ` M ) e. _V /\ ( x ( .s ` M ) y ) e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` ( x ( .s ` M ) y ) ) = ( ( F ` ( x ( .s ` M ) y ) ) .+ ( G ` ( x ( .s ` M ) y ) ) ) )
53 46 47 48 51 52 syl22anc 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` ( x ( .s ` M ) y ) ) = ( ( F ` ( x ( .s ` M ) y ) ) .+ ( G ` ( x ( .s ` M ) y ) ) ) )
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 46 47 48 24 54 syl22anc 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` y ) = ( ( F ` y ) .+ ( G ` y ) ) )
56 55 oveq2d 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( x ( .s ` N ) ( ( F oF .+ G ) ` y ) ) = ( x ( .s ` N ) ( ( F ` y ) .+ ( G ` y ) ) ) )
57 45 53 56 3eqtr4d 
 |-  ( ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( ( F oF .+ G ) ` ( x ( .s ` M ) y ) ) = ( x ( .s ` N ) ( ( F oF .+ G ) ` y ) ) )
58 2 3 4 5 6 7 9 11 13 21 57 islmhmd 
 |-  ( ( F e. ( M LMHom N ) /\ G e. ( M LMHom N ) ) -> ( F oF .+ G ) e. ( M LMHom N ) )