lmodvs0

Description: Anything times the zero vector is the zero vector. Equation 1b of Kreyszig p. 51. ( hvmul0 analog.) (Contributed by NM, 12-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmodvs0.f	$⊢ F = Scalar (W)$
	lmodvs0.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lmodvs0.k	$⊢ K = {Base}_{F}$
	lmodvs0.z	$⊢ \underset{˙}{0} = 0_{W}$
Assertion	lmodvs0	$⊢ (W \in LMod \land X \in K) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		lmodvs0.f	$⊢ F = Scalar (W)$
2		lmodvs0.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		lmodvs0.k	$⊢ K = {Base}_{F}$
4		lmodvs0.z	$⊢ \underset{˙}{0} = 0_{W}$
5	1	lmodring	$⊢ W \in LMod \to F \in Ring$
6		eqid	$⊢ \cdot_{F} = \cdot_{F}$
7		eqid	$⊢ 0_{F} = 0_{F}$
8	3 6 7	ringrz	$⊢ (F \in Ring \land X \in K) \to X \cdot_{F} 0_{F} = 0_{F}$
9	5 8	sylan	$⊢ (W \in LMod \land X \in K) \to X \cdot_{F} 0_{F} = 0_{F}$
10	9	oveq1d	$⊢ (W \in LMod \land X \in K) \to (X \cdot_{F} 0_{F}) \underset{˙}{\cdot} \underset{˙}{0} = 0_{F} \underset{˙}{\cdot} \underset{˙}{0}$
11		simpl	$⊢ (W \in LMod \land X \in K) \to W \in LMod$
12		simpr	$⊢ (W \in LMod \land X \in K) \to X \in K$
13	5	adantr	$⊢ (W \in LMod \land X \in K) \to F \in Ring$
14	3 7	ring0cl	$⊢ F \in Ring \to 0_{F} \in K$
15	13 14	syl	$⊢ (W \in LMod \land X \in K) \to 0_{F} \in K$
16		eqid	$⊢ {Base}_{W} = {Base}_{W}$
17	16 4	lmod0vcl	$⊢ W \in LMod \to \underset{˙}{0} \in {Base}_{W}$
18	17	adantr	$⊢ (W \in LMod \land X \in K) \to \underset{˙}{0} \in {Base}_{W}$
19	16 1 2 3 6	lmodvsass	$⊢ (W \in LMod \land (X \in K \land 0_{F} \in K \land \underset{˙}{0} \in {Base}_{W})) \to (X \cdot_{F} 0_{F}) \underset{˙}{\cdot} \underset{˙}{0} = X \underset{˙}{\cdot} (0_{F} \underset{˙}{\cdot} \underset{˙}{0})$
20	11 12 15 18 19	syl13anc	$⊢ (W \in LMod \land X \in K) \to (X \cdot_{F} 0_{F}) \underset{˙}{\cdot} \underset{˙}{0} = X \underset{˙}{\cdot} (0_{F} \underset{˙}{\cdot} \underset{˙}{0})$
21	16 1 2 7 4	lmod0vs	$⊢ (W \in LMod \land \underset{˙}{0} \in {Base}_{W}) \to 0_{F} \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
22	18 21	syldan	$⊢ (W \in LMod \land X \in K) \to 0_{F} \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
23	22	oveq2d	$⊢ (W \in LMod \land X \in K) \to X \underset{˙}{\cdot} (0_{F} \underset{˙}{\cdot} \underset{˙}{0}) = X \underset{˙}{\cdot} \underset{˙}{0}$
24	20 23	eqtrd	$⊢ (W \in LMod \land X \in K) \to (X \cdot_{F} 0_{F}) \underset{˙}{\cdot} \underset{˙}{0} = X \underset{˙}{\cdot} \underset{˙}{0}$
25	10 24 22	3eqtr3d	$⊢ (W \in LMod \land X \in K) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$

Metamath Proof Explorer

Theorem lmodvs0

Proof