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={\mathrm{Base}}_W$$
	slmd0vs.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	slmd0vs.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	slmd0vs.o	$$⊢O=0_F$$
	slmd0vs.z	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	slmd0vs	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to O\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		slmd0vs.v	$$⊢V={\mathrm{Base}}_W$$
2		slmd0vs.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		slmd0vs.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		slmd0vs.o	$$⊢O=0_F$$
5		slmd0vs.z	$$⊢\underset{\dot{}}{0}=0_W$$
6		simpl	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to W\in \mathrm{SLMod}$$
7		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
8	2 7 4	slmd0cl	$$⊢W\in \mathrm{SLMod}\to O\in {\mathrm{Base}}_F$$
9	8	adantr	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to O\in {\mathrm{Base}}_F$$
10		simpr	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\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	$$⊢\left(W\in \mathrm{SLMod}\wedge \left(O\in {\mathrm{Base}}_F\wedge O\in {\mathrm{Base}}_F\right)\wedge \left(X\in V\wedge X\in V\right)\right)\to \left(\left(O\underset{\dot{}}{·}X\in V\wedge O\underset{\dot{}}{·}\left(X{+}_{W}X\right)=\left(O\underset{\dot{}}{·}X\right){+}_W\left(O\underset{\dot{}}{·}X\right)\wedge \left(O{+}_{F}O\right)\underset{\dot{}}{·}X=\left(O\underset{\dot{}}{·}X\right){+}_W\left(O\underset{\dot{}}{·}X\right)\right)\wedge \left(\left(O{\cdot }_{F}O\right)\underset{\dot{}}{·}X=O\underset{\dot{}}{·}\left(O\underset{\dot{}}{·}X\right)\wedge 1_F\underset{\dot{}}{·}X=X\wedge O\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\right)$$
16	6 9 9 10 10 15	syl122anc	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to \left(\left(O\underset{\dot{}}{·}X\in V\wedge O\underset{\dot{}}{·}\left(X{+}_{W}X\right)=\left(O\underset{\dot{}}{·}X\right){+}_W\left(O\underset{\dot{}}{·}X\right)\wedge \left(O{+}_{F}O\right)\underset{\dot{}}{·}X=\left(O\underset{\dot{}}{·}X\right){+}_W\left(O\underset{\dot{}}{·}X\right)\right)\wedge \left(\left(O{\cdot }_{F}O\right)\underset{\dot{}}{·}X=O\underset{\dot{}}{·}\left(O\underset{\dot{}}{·}X\right)\wedge 1_F\underset{\dot{}}{·}X=X\wedge O\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\right)$$
17	16	simprd	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to \left(\left(O{\cdot }_{F}O\right)\underset{\dot{}}{·}X=O\underset{\dot{}}{·}\left(O\underset{\dot{}}{·}X\right)\wedge 1_F\underset{\dot{}}{·}X=X\wedge O\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)$$
18	17	simp3d	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in V\right)\to O\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$