This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmhmco

Description: The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Assertion lmhmco ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑀 LMHom 𝑂 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
2 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
3 eqid ⊢ ( ·𝑠 ‘ 𝑂 ) = ( ·𝑠 ‘ 𝑂 )
4 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
5 eqid ⊢ ( Scalar ‘ 𝑂 ) = ( Scalar ‘ 𝑂 )
6 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
7 lmhmlmod1 ⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝑀 ∈ LMod )
8 7 adantl ⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑀 ∈ LMod )
9 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) → 𝑂 ∈ LMod )
10 9 adantr ⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑂 ∈ LMod )
11 eqid ⊢ ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑁 )
12 11 5 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) → ( Scalar ‘ 𝑂 ) = ( Scalar ‘ 𝑁 ) )
13 4 11 lmhmsca ⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑀 ) )
14 12 13 sylan9eq ⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( Scalar ‘ 𝑂 ) = ( Scalar ‘ 𝑀 ) )
15 lmghm ⊢ ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) → 𝐹 ∈ ( 𝑁 GrpHom 𝑂 ) )
16 lmghm ⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) )
17 ghmco ⊢ ( ( 𝐹 ∈ ( 𝑁 GrpHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑀 GrpHom 𝑂 ) )
18 15 16 17 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑀 GrpHom 𝑂 ) )
19 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) )
20 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
21 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑀 ) )
22 eqid ⊢ ( ·𝑠 ‘ 𝑁 ) = ( ·𝑠 ‘ 𝑁 )
23 4 6 1 2 22 lmhmlin ⊢ ( ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) )
24 19 20 21 23 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) )
25 24 fveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) )
26 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) )
27 13 fveq2d ⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
28 27 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
29 20 28 eleqtrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑁 ) ) )
30 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
31 1 30 lmhmf ⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
32 31 adantl ⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
33 32 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
34 33 adantrl ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
35 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑁 ) )
36 11 35 30 22 3 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑁 ) ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
37 26 29 34 36 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
38 25 37 eqtrd ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
39 32 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐺 Fn ( Base ‘ 𝑀 ) )
40 7 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LMod )
41 1 4 2 6 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
42 40 20 21 41 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
43 fvco2 ⊢ ( ( 𝐺 Fn ( Base ‘ 𝑀 ) ∧ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
44 39 42 43 syl2an2r ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
45 fvco2 ⊢ ( ( 𝐺 Fn ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
46 39 21 45 syl2an2r ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
47 46 oveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
48 38 44 47 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) )
49 1 2 3 4 5 6 8 10 14 18 48 islmhmd ⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑀 LMHom 𝑂 ) )