0lmhm

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

	Ref	Expression
Hypotheses	0lmhm.z	$⊢ \underset{˙}{0} = 0_{N}$
	0lmhm.b	$⊢ B = {Base}_{M}$
	0lmhm.s	$⊢ S = Scalar (M)$
	0lmhm.t	$⊢ T = Scalar (N)$
Assertion	0lmhm	$⊢ (M \in LMod \land N \in LMod \land S = T) \to B \times \{\underset{˙}{0}\} \in (M LMHom N)$

Proof

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

Metamath Proof Explorer

Theorem 0lmhm

Proof