0lmhm

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

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

Proof

Step	Hyp	Ref	Expression
1		0lmhm.z	⊢ 0 = ( 0_g ‘ 𝑁 )
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 𝑁 ) )

Metamath Proof Explorer

Theorem 0lmhm

Proof