Theorem lcd0vs

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

	Ref	Expression
Hypotheses	lcd0vs.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcd0vs.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcd0vs.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	lcd0vs.z	$$⊢\underset{\dot{}}{0}=0_R$$
	lcd0vs.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcd0vs.v	$$⊢V={\mathrm{Base}}_C$$
	lcd0vs.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
	lcd0vs.o	$$⊢O=0_C$$
	lcd0vs.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcd0vs.g	$$⊢\phi \to G\in V$$
Assertion	lcd0vs	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}G=O$$

Proof

Step	Hyp	Ref	Expression
1		lcd0vs.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcd0vs.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcd0vs.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
4		lcd0vs.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		lcd0vs.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		lcd0vs.v	$$⊢V={\mathrm{Base}}_C$$
7		lcd0vs.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
8		lcd0vs.o	$$⊢O=0_C$$
9		lcd0vs.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lcd0vs.g	$$⊢\phi \to G\in V$$
11		eqid	$$⊢\mathrm{Scalar}\left(C\right)=\mathrm{Scalar}\left(C\right)$$
12		eqid	$$⊢0_{\mathrm{Scalar}\left(C\right)}=0_{\mathrm{Scalar}\left(C\right)}$$
13	1 2 3 4 5 11 12 9	lcd0	$$⊢\phi \to 0_{\mathrm{Scalar}\left(C\right)}=\underset{\dot{}}{0}$$
14	13	oveq1d	$$⊢\phi \to 0_{\mathrm{Scalar}\left(C\right)}\underset{\dot{}}{·}G=\underset{\dot{}}{0}\underset{\dot{}}{·}G$$
15	1 5 9	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
16	6 11 7 12 8	lmod0vs	$$⊢\left(C\in \mathrm{LMod}\wedge G\in V\right)\to 0_{\mathrm{Scalar}\left(C\right)}\underset{\dot{}}{·}G=O$$
17	15 10 16	syl2anc	$$⊢\phi \to 0_{\mathrm{Scalar}\left(C\right)}\underset{\dot{}}{·}G=O$$
18	14 17	eqtr3d	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}G=O$$