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 ‘ 𝑁 )
Assertion lmhmplusg ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 LMHom 𝑁 ) )

Proof

Step Hyp Ref Expression
1 lmhmplusg.p ⊢ + = ( +g ‘ 𝑁 )
2 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
4 eqid ⊢ ( ·𝑠 ‘ 𝑁 ) = ( ·𝑠 ‘ 𝑁 )
5 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
6 eqid ⊢ ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑁 )
7 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
8 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝑀 ∈ LMod )
9 8 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑀 ∈ LMod )
10 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝑁 ∈ LMod )
11 10 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑁 ∈ LMod )
12 5 6 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑀 ) )
13 12 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑀 ) )
14 lmodabl ⊢ ( 𝑁 ∈ LMod → 𝑁 ∈ Abel )
15 11 14 syl ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑁 ∈ Abel )
16 lmghm ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
17 16 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
18 lmghm ⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) )
19 18 adantl ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) )
20 1 ghmplusg ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 GrpHom 𝑁 ) )
21 15 17 19 20 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 GrpHom 𝑁 ) )
22 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) )
23 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
24 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑀 ) )
25 5 7 2 3 4 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) )
26 22 23 24 25 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) )
27 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) )
28 5 7 2 3 4 lmhmlin ⊢ ( ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) )
29 27 23 24 28 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) )
30 26 29 oveq12d ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) + ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) )
31 10 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑁 ∈ LMod )
32 12 fveq2d ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
33 32 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
34 23 33 eleqtrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑁 ) ) )
35 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
36 2 35 lmhmf ⊢ ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
37 36 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
38 37 24 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
39 2 35 lmhmf ⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
40 39 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
41 40 24 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
42 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑁 ) )
43 35 1 6 4 42 lmodvsdi ⊢ ( ( 𝑁 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑁 ) ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) + ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) )
44 31 34 38 41 43 syl13anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) + ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) )
45 30 44 eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) )
46 37 ffnd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
47 40 ffnd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 Fn ( Base ‘ 𝑀 ) )
48 fvexd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( Base ‘ 𝑀 ) ∈ V )
49 8 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LMod )
50 2 5 3 7 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
51 49 23 24 50 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
52 fnfvof ⊢ ( ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝐺 Fn ( Base ‘ 𝑀 ) ) ∧ ( ( Base ‘ 𝑀 ) ∈ V ∧ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
53 46 47 48 51 52 syl22anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
54 fnfvof ⊢ ( ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝐺 Fn ( Base ‘ 𝑀 ) ) ∧ ( ( Base ‘ 𝑀 ) ∈ V ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) )
55 46 47 48 24 54 syl22anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) )
56 55 oveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) )
57 45 53 56 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) ) )
58 2 3 4 5 6 7 9 11 13 21 57 islmhmd ⊢ ( ( 𝐹 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 LMHom 𝑁 ) )