slmdvs0

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) (Revised by Thierry Arnoux, 1-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		slmdvs0.f	$⊢ F = Scalar (W)$
2		slmdvs0.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		slmdvs0.k	$⊢ K = {Base}_{F}$
4		slmdvs0.z	$⊢ \underset{˙}{0} = 0_{W}$
5	1	slmdsrg	$⊢ W \in SLMod \to F \in SRing$
6		eqid	$⊢ \cdot_{F} = \cdot_{F}$
7		eqid	$⊢ 0_{F} = 0_{F}$
8	3 6 7	srgrz	$⊢ (F \in SRing \land X \in K) \to X \cdot_{F} 0_{F} = 0_{F}$
9	5 8	sylan	$⊢ (W \in SLMod \land X \in K) \to X \cdot_{F} 0_{F} = 0_{F}$
10	9	oveq1d	$⊢ (W \in SLMod \land X \in K) \to (X \cdot_{F} 0_{F}) \underset{˙}{\cdot} \underset{˙}{0} = 0_{F} \underset{˙}{\cdot} \underset{˙}{0}$
11		simpl	$⊢ (W \in SLMod \land X \in K) \to W \in SLMod$
12		simpr	$⊢ (W \in SLMod \land X \in K) \to X \in K$
13	5	adantr	$⊢ (W \in SLMod \land X \in K) \to F \in SRing$
14	3 7	srg0cl	$⊢ F \in SRing \to 0_{F} \in K$
15	13 14	syl	$⊢ (W \in SLMod \land X \in K) \to 0_{F} \in K$
16		eqid	$⊢ {Base}_{W} = {Base}_{W}$
17	16 4	slmd0vcl	$⊢ W \in SLMod \to \underset{˙}{0} \in {Base}_{W}$
18	17	adantr	$⊢ (W \in SLMod \land X \in K) \to \underset{˙}{0} \in {Base}_{W}$
19	16 1 2 3 6	slmdvsass	$⊢ (W \in SLMod \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 SLMod \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	slmd0vs	$⊢ (W \in SLMod \land \underset{˙}{0} \in {Base}_{W}) \to 0_{F} \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
22	18 21	syldan	$⊢ (W \in SLMod \land X \in K) \to 0_{F} \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
23	22	oveq2d	$⊢ (W \in SLMod \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 SLMod \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 SLMod \land X \in K) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$

Metamath Proof Explorer

Theorem slmdvs0

Proof