Theorem lcdvs0N

Description: A scalar times the zero functional is the zero functional. (Contributed by NM, 20-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lcdvs0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdvs0.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdvs0.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcdvs0.r	$$⊢R={\mathrm{Base}}_S$$
	lcdvs0.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdvs0.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
	lcdvs0.o	$$⊢\underset{\dot{}}{0}=0_C$$
	lcdvs0.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdvs0.x	$$⊢\phi \to X\in R$$
Assertion	lcdvs0N	$$⊢\phi \to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lcdvs0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvs0.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdvs0.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
4		lcdvs0.r	$$⊢R={\mathrm{Base}}_S$$
5		lcdvs0.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		lcdvs0.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
7		lcdvs0.o	$$⊢\underset{\dot{}}{0}=0_C$$
8		lcdvs0.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		lcdvs0.x	$$⊢\phi \to X\in R$$
10	1 5 8	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
11		eqid	$$⊢\mathrm{Scalar}\left(C\right)=\mathrm{Scalar}\left(C\right)$$
12		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
13	1 2 3 4 5 11 12 8	lcdsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}=R$$
14	9 13	eleqtrrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
15	11 6 12 7	lmodvs0	$$⊢\left(C\in \mathrm{LMod}\wedge X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
16	10 14 15	syl2anc	$$⊢\phi \to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$