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

Proof

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