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 ` N )
0lmhm.b 
|- B = ( Base ` M )
0lmhm.s 
|- S = ( Scalar ` M )
0lmhm.t 
|- T = ( Scalar ` N )
Assertion 0lmhm 
|- ( ( M e. LMod /\ N e. LMod /\ S = T ) -> ( B X. { .0. } ) e. ( M LMHom N ) )

Proof

Step Hyp Ref Expression
1 0lmhm.z 
 |-  .0. = ( 0g ` N )
2 0lmhm.b 
 |-  B = ( Base ` M )
3 0lmhm.s 
 |-  S = ( Scalar ` M )
4 0lmhm.t 
 |-  T = ( Scalar ` N )
5 eqid 
 |-  ( .s ` M ) = ( .s ` M )
6 eqid 
 |-  ( .s ` N ) = ( .s ` N )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 simp1 
 |-  ( ( M e. LMod /\ N e. LMod /\ S = T ) -> M e. LMod )
9 simp2 
 |-  ( ( M e. LMod /\ N e. LMod /\ S = T ) -> N e. LMod )
10 simp3 
 |-  ( ( M e. LMod /\ N e. LMod /\ S = T ) -> S = T )
11 10 eqcomd 
 |-  ( ( M e. LMod /\ N e. LMod /\ S = T ) -> T = S )
12 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
13 lmodgrp 
 |-  ( N e. LMod -> N e. Grp )
14 1 2 0ghm 
 |-  ( ( M e. Grp /\ N e. Grp ) -> ( B X. { .0. } ) e. ( M GrpHom N ) )
15 12 13 14 syl2an 
 |-  ( ( M e. LMod /\ N e. LMod ) -> ( B X. { .0. } ) e. ( M GrpHom N ) )
16 15 3adant3 
 |-  ( ( M e. LMod /\ N e. LMod /\ S = T ) -> ( B X. { .0. } ) e. ( M GrpHom N ) )
17 simpl2 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> N e. LMod )
18 simprl 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> x e. ( Base ` S ) )
19 simpl3 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> S = T )
20 19 fveq2d 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> ( Base ` S ) = ( Base ` T ) )
21 18 20 eleqtrd 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> x e. ( Base ` T ) )
22 eqid 
 |-  ( Base ` T ) = ( Base ` T )
23 4 6 22 1 lmodvs0 
 |-  ( ( N e. LMod /\ x e. ( Base ` T ) ) -> ( x ( .s ` N ) .0. ) = .0. )
24 17 21 23 syl2anc 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> ( x ( .s ` N ) .0. ) = .0. )
25 1 fvexi 
 |-  .0. e. _V
26 25 fvconst2 
 |-  ( y e. B -> ( ( B X. { .0. } ) ` y ) = .0. )
27 26 oveq2d 
 |-  ( y e. B -> ( x ( .s ` N ) ( ( B X. { .0. } ) ` y ) ) = ( x ( .s ` N ) .0. ) )
28 27 ad2antll 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> ( x ( .s ` N ) ( ( B X. { .0. } ) ` y ) ) = ( x ( .s ` N ) .0. ) )
29 simpl1 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> M e. LMod )
30 simprr 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> y e. B )
31 2 3 5 7 lmodvscl 
 |-  ( ( M e. LMod /\ x e. ( Base ` S ) /\ y e. B ) -> ( x ( .s ` M ) y ) e. B )
32 29 18 30 31 syl3anc 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> ( x ( .s ` M ) y ) e. B )
33 25 fvconst2 
 |-  ( ( x ( .s ` M ) y ) e. B -> ( ( B X. { .0. } ) ` ( x ( .s ` M ) y ) ) = .0. )
34 32 33 syl 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> ( ( B X. { .0. } ) ` ( x ( .s ` M ) y ) ) = .0. )
35 24 28 34 3eqtr4rd 
 |-  ( ( ( M e. LMod /\ N e. LMod /\ S = T ) /\ ( x e. ( Base ` S ) /\ y e. B ) ) -> ( ( B X. { .0. } ) ` ( x ( .s ` M ) y ) ) = ( x ( .s ` N ) ( ( B X. { .0. } ) ` y ) ) )
36 2 5 6 3 4 7 8 9 11 16 35 islmhmd 
 |-  ( ( M e. LMod /\ N e. LMod /\ S = T ) -> ( B X. { .0. } ) e. ( M LMHom N ) )