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

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 𝑁 ) )