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

Metamath Proof Explorer

Theorem slmd0vs

Description: Zero times a vector is the zero vector. Equation 1a of Kreyszig p. 51. ( ax-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	slmd0vs.v	$⊢ V = {Base}_{W}$
		slmd0vs.f	$⊢ F = Scalar (W)$
		slmd0vs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
		slmd0vs.o	$⊢ O = 0_{F}$
		slmd0vs.z	$⊢ \underset{˙}{0} = 0_{W}$
	Assertion	slmd0vs	$⊢ (W \in SLMod \land X \in V) \to O \underset{˙}{\cdot} X = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		slmd0vs.v	$⊢ V = {Base}_{W}$
2		slmd0vs.f	$⊢ F = Scalar (W)$
3		slmd0vs.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		slmd0vs.o	$⊢ O = 0_{F}$
5		slmd0vs.z	$⊢ \underset{˙}{0} = 0_{W}$
6		simpl	$⊢ (W \in SLMod \land X \in V) \to W \in SLMod$
7		eqid	$⊢ {Base}_{F} = {Base}_{F}$
8	2 7 4	slmd0cl	$⊢ W \in SLMod \to O \in {Base}_{F}$
9	8	adantr	$⊢ (W \in SLMod \land X \in V) \to O \in {Base}_{F}$
10		simpr	$⊢ (W \in SLMod \land X \in V) \to X \in V$
11		eqid	$⊢ +_{W} = +_{W}$
12		eqid	$⊢ +_{F} = +_{F}$
13		eqid	$⊢ \cdot_{F} = \cdot_{F}$
14		eqid	$⊢ 1_{F} = 1_{F}$
15	1 11 3 5 2 7 12 13 14 4	slmdlema	$⊢ (W \in SLMod \land (O \in {Base}_{F} \land O \in {Base}_{F}) \land (X \in V \land X \in V)) \to ((O \underset{˙}{\cdot} X \in V \land O \underset{˙}{\cdot} (X +_{W} X) = (O \underset{˙}{\cdot} X) +_{W} (O \underset{˙}{\cdot} X) \land (O +_{F} O) \underset{˙}{\cdot} X = (O \underset{˙}{\cdot} X) +_{W} (O \underset{˙}{\cdot} X)) \land ((O \cdot_{F} O) \underset{˙}{\cdot} X = O \underset{˙}{\cdot} (O \underset{˙}{\cdot} X) \land 1_{F} \underset{˙}{\cdot} X = X \land O \underset{˙}{\cdot} X = \underset{˙}{0}))$
16	6 9 9 10 10 15	syl122anc	$⊢ (W \in SLMod \land X \in V) \to ((O \underset{˙}{\cdot} X \in V \land O \underset{˙}{\cdot} (X +_{W} X) = (O \underset{˙}{\cdot} X) +_{W} (O \underset{˙}{\cdot} X) \land (O +_{F} O) \underset{˙}{\cdot} X = (O \underset{˙}{\cdot} X) +_{W} (O \underset{˙}{\cdot} X)) \land ((O \cdot_{F} O) \underset{˙}{\cdot} X = O \underset{˙}{\cdot} (O \underset{˙}{\cdot} X) \land 1_{F} \underset{˙}{\cdot} X = X \land O \underset{˙}{\cdot} X = \underset{˙}{0}))$
17	16	simprd	$⊢ (W \in SLMod \land X \in V) \to ((O \cdot_{F} O) \underset{˙}{\cdot} X = O \underset{˙}{\cdot} (O \underset{˙}{\cdot} X) \land 1_{F} \underset{˙}{\cdot} X = X \land O \underset{˙}{\cdot} X = \underset{˙}{0})$
18	17	simp3d	$⊢ (W \in SLMod \land X \in V) \to O \underset{˙}{\cdot} X = \underset{˙}{0}$