This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clm0vs

Description: Zero times a vector is the zero vector. Equation 1a of Kreyszig p. 51. ( lmod0vs analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

		Ref	Expression
	Hypotheses	clm0vs.v	$⊢ V = {Base}_{W}$
		clm0vs.f	$⊢ F = Scalar (W)$
		clm0vs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
		clm0vs.z	$⊢ \underset{˙}{0} = 0_{W}$
	Assertion	clm0vs	$⊢ (W \in CMod \land X \in V) \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		clm0vs.v	$⊢ V = {Base}_{W}$
2		clm0vs.f	$⊢ F = Scalar (W)$
3		clm0vs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		clm0vs.z	$⊢ \underset{˙}{0} = 0_{W}$
5	2	clm0	$⊢ W \in CMod \to 0 = 0_{F}$
6	5	adantr	$⊢ (W \in CMod \land X \in V) \to 0 = 0_{F}$
7	6	oveq1d	$⊢ (W \in CMod \land X \in V) \to 0 \underset{˙}{\cdot} X = 0_{F} \underset{˙}{\cdot} X$
8		clmlmod	$⊢ W \in CMod \to W \in LMod$
9		eqid	$⊢ 0_{F} = 0_{F}$
10	1 2 3 9 4	lmod0vs	$⊢ (W \in LMod \land X \in V) \to 0_{F} \underset{˙}{\cdot} X = \underset{˙}{0}$
11	8 10	sylan	$⊢ (W \in CMod \land X \in V) \to 0_{F} \underset{˙}{\cdot} X = \underset{˙}{0}$
12	7 11	eqtrd	$⊢ (W \in CMod \land X \in V) \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$