Theorem lmodvs0

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)

	Ref	Expression
Hypotheses	lmodvs0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lmodvs0.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lmodvs0.k	$$⊢K={\mathrm{Base}}_F$$
	lmodvs0.z	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	lmodvs0	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lmodvs0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		lmodvs0.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		lmodvs0.k	$$⊢K={\mathrm{Base}}_F$$
4		lmodvs0.z	$$⊢\underset{\dot{}}{0}=0_W$$
5	1	lmodring	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$
6		eqid	$$⊢{\cdot }_F={\cdot }_F$$
7		eqid	$$⊢0_F=0_F$$
8	3 6 7	ringrz	$$⊢\left(F\in \mathrm{Ring}\wedge X\in K\right)\to X{\cdot }_F{0}_F=0_F$$
9	5 8	sylan	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to X{\cdot }_F{0}_F=0_F$$
10	9	oveq1d	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to \left(X{\cdot }_F{0}_F\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=0_F\underset{\dot{}}{·}\underset{\dot{}}{0}$$
11		simpl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to W\in \mathrm{LMod}$$
12		simpr	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to X\in K$$
13	5	adantr	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to F\in \mathrm{Ring}$$
14	3 7	ring0cl	$$⊢F\in \mathrm{Ring}\to 0_F\in K$$
15	13 14	syl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to 0_F\in K$$
16		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
17	16 4	lmod0vcl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_W$$
18	17	adantr	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_W$$
19	16 1 2 3 6	lmodvsass	$$⊢\left(W\in \mathrm{LMod}\wedge \left(X\in K\wedge 0_F\in K\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_W\right)\right)\to \left(X{\cdot }_F{0}_F\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=X\underset{\dot{}}{·}\left(0_F\underset{\dot{}}{·}\underset{\dot{}}{0}\right)$$
20	11 12 15 18 19	syl13anc	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to \left(X{\cdot }_F{0}_F\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=X\underset{\dot{}}{·}\left(0_F\underset{\dot{}}{·}\underset{\dot{}}{0}\right)$$
21	16 1 2 7 4	lmod0vs	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_W\right)\to 0_F\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
22	18 21	syldan	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to 0_F\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
23	22	oveq2d	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to X\underset{\dot{}}{·}\left(0_F\underset{\dot{}}{·}\underset{\dot{}}{0}\right)=X\underset{\dot{}}{·}\underset{\dot{}}{0}$$
24	20 23	eqtrd	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to \left(X{\cdot }_F{0}_F\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=X\underset{\dot{}}{·}\underset{\dot{}}{0}$$
25	10 24 22	3eqtr3d	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$