Theorem slmdvs0

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) (Revised by Thierry Arnoux, 1-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		slmdvs0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		slmdvs0.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		slmdvs0.k	$$⊢K={\mathrm{Base}}_F$$
4		slmdvs0.z	$$⊢\underset{\dot{}}{0}=0_W$$
5	1	slmdsrg	$$⊢W\in \mathrm{SLMod}\to F\in \mathrm{SRing}$$
6		eqid	$$⊢{\cdot }_F={\cdot }_F$$
7		eqid	$$⊢0_F=0_F$$
8	3 6 7	srgrz	$$⊢\left(F\in \mathrm{SRing}\wedge X\in K\right)\to X{\cdot }_F{0}_F=0_F$$
9	5 8	sylan	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in K\right)\to X{\cdot }_F{0}_F=0_F$$
10	9	oveq1d	$$⊢\left(W\in \mathrm{SLMod}\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{SLMod}\wedge X\in K\right)\to W\in \mathrm{SLMod}$$
12		simpr	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in K\right)\to X\in K$$
13	5	adantr	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in K\right)\to F\in \mathrm{SRing}$$
14	3 7	srg0cl	$$⊢F\in \mathrm{SRing}\to 0_F\in K$$
15	13 14	syl	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in K\right)\to 0_F\in K$$
16		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
17	16 4	slmd0vcl	$$⊢W\in \mathrm{SLMod}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_W$$
18	17	adantr	$$⊢\left(W\in \mathrm{SLMod}\wedge X\in K\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_W$$
19	16 1 2 3 6	slmdvsass	$$⊢\left(W\in \mathrm{SLMod}\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{SLMod}\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	slmd0vs	$$⊢\left(W\in \mathrm{SLMod}\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{SLMod}\wedge X\in K\right)\to 0_F\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
23	22	oveq2d	$$⊢\left(W\in \mathrm{SLMod}\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{SLMod}\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{SLMod}\wedge X\in K\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$