Metamath Proof Explorer


Theorem 0lmhm

Description: The constant zero linear function between two modules. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses 0lmhm.z 0 = ( 0g𝑁 )
0lmhm.b 𝐵 = ( Base ‘ 𝑀 )
0lmhm.s 𝑆 = ( Scalar ‘ 𝑀 )
0lmhm.t 𝑇 = ( Scalar ‘ 𝑁 )
Assertion 0lmhm ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 LMHom 𝑁 ) )

Proof

Step Hyp Ref Expression
1 0lmhm.z 0 = ( 0g𝑁 )
2 0lmhm.b 𝐵 = ( Base ‘ 𝑀 )
3 0lmhm.s 𝑆 = ( Scalar ‘ 𝑀 )
4 0lmhm.t 𝑇 = ( Scalar ‘ 𝑁 )
5 eqid ( ·𝑠𝑀 ) = ( ·𝑠𝑀 )
6 eqid ( ·𝑠𝑁 ) = ( ·𝑠𝑁 )
7 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8 simp1 ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) → 𝑀 ∈ LMod )
9 simp2 ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) → 𝑁 ∈ LMod )
10 simp3 ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) → 𝑆 = 𝑇 )
11 10 eqcomd ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) → 𝑇 = 𝑆 )
12 lmodgrp ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
13 lmodgrp ( 𝑁 ∈ LMod → 𝑁 ∈ Grp )
14 1 2 0ghm ( ( 𝑀 ∈ Grp ∧ 𝑁 ∈ Grp ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 GrpHom 𝑁 ) )
15 12 13 14 syl2an ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 GrpHom 𝑁 ) )
16 15 3adant3 ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 GrpHom 𝑁 ) )
17 simpl2 ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑁 ∈ LMod )
18 simprl ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
19 simpl3 ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑆 = 𝑇 )
20 19 fveq2d ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑇 ) )
21 18 20 eleqtrd ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝑇 ) )
22 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
23 4 6 22 1 lmodvs0 ( ( 𝑁 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑇 ) ) → ( 𝑥 ( ·𝑠𝑁 ) 0 ) = 0 )
24 17 21 23 syl2anc ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → ( 𝑥 ( ·𝑠𝑁 ) 0 ) = 0 )
25 1 fvexi 0 ∈ V
26 25 fvconst2 ( 𝑦𝐵 → ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) = 0 )
27 26 oveq2d ( 𝑦𝐵 → ( 𝑥 ( ·𝑠𝑁 ) ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠𝑁 ) 0 ) )
28 27 ad2antll ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → ( 𝑥 ( ·𝑠𝑁 ) ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠𝑁 ) 0 ) )
29 simpl1 ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑀 ∈ LMod )
30 simprr ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑦𝐵 )
31 2 3 5 7 lmodvscl ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) → ( 𝑥 ( ·𝑠𝑀 ) 𝑦 ) ∈ 𝐵 )
32 29 18 30 31 syl3anc ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → ( 𝑥 ( ·𝑠𝑀 ) 𝑦 ) ∈ 𝐵 )
33 25 fvconst2 ( ( 𝑥 ( ·𝑠𝑀 ) 𝑦 ) ∈ 𝐵 → ( ( 𝐵 × { 0 } ) ‘ ( 𝑥 ( ·𝑠𝑀 ) 𝑦 ) ) = 0 )
34 32 33 syl ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → ( ( 𝐵 × { 0 } ) ‘ ( 𝑥 ( ·𝑠𝑀 ) 𝑦 ) ) = 0 )
35 24 28 34 3eqtr4rd ( ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦𝐵 ) ) → ( ( 𝐵 × { 0 } ) ‘ ( 𝑥 ( ·𝑠𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠𝑁 ) ( ( 𝐵 × { 0 } ) ‘ 𝑦 ) ) )
36 2 5 6 3 4 7 8 9 11 16 35 islmhmd ( ( 𝑀 ∈ LMod ∧ 𝑁 ∈ LMod ∧ 𝑆 = 𝑇 ) → ( 𝐵 × { 0 } ) ∈ ( 𝑀 LMHom 𝑁 ) )