Theorem ldual0vs

Description: Scalar zero times a functional is the zero functional. (Contributed by NM, 17-Feb-2015)

	Ref	Expression
Hypotheses	ldual0vs.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldual0vs.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldual0vs.z	$$⊢\underset{\dot{}}{0}=0_R$$
	ldual0vs.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldual0vs.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	ldual0vs.o	$$⊢O=0_D$$
	ldual0vs.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldual0vs.g	$$⊢\phi \to G\in F$$
Assertion	ldual0vs	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}G=O$$

Proof

Step	Hyp	Ref	Expression
1		ldual0vs.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldual0vs.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		ldual0vs.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		ldual0vs.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
5		ldual0vs.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
6		ldual0vs.o	$$⊢O=0_D$$
7		ldual0vs.w	$$⊢\phi \to W\in \mathrm{LMod}$$
8		ldual0vs.g	$$⊢\phi \to G\in F$$
9		eqid	$$⊢\mathrm{Scalar}\left(D\right)=\mathrm{Scalar}\left(D\right)$$
10		eqid	$$⊢0_{\mathrm{Scalar}\left(D\right)}=0_{\mathrm{Scalar}\left(D\right)}$$
11	2 3 4 9 10 7	ldual0	$$⊢\phi \to 0_{\mathrm{Scalar}\left(D\right)}=\underset{\dot{}}{0}$$
12	11	oveq1d	$$⊢\phi \to 0_{\mathrm{Scalar}\left(D\right)}\underset{\dot{}}{·}G=\underset{\dot{}}{0}\underset{\dot{}}{·}G$$
13	4 7	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$
14		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
15	1 4 14 7 8	ldualelvbase	$$⊢\phi \to G\in {\mathrm{Base}}_D$$
16	14 9 5 10 6	lmod0vs	$$⊢\left(D\in \mathrm{LMod}\wedge G\in {\mathrm{Base}}_D\right)\to 0_{\mathrm{Scalar}\left(D\right)}\underset{\dot{}}{·}G=O$$
17	13 15 16	syl2anc	$$⊢\phi \to 0_{\mathrm{Scalar}\left(D\right)}\underset{\dot{}}{·}G=O$$
18	12 17	eqtr3d	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}G=O$$