Theorem ldual0vcl

Description: The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015)

	Ref	Expression
Hypotheses	ldualv0cl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualv0cl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualv0cl.o	$$⊢\underset{\dot{}}{0}=0_D$$
	ldualv0cl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
Assertion	ldual0vcl	$$⊢\phi \to \underset{\dot{}}{0}\in F$$

Proof

Step	Hyp	Ref	Expression
1		ldualv0cl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualv0cl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
3		ldualv0cl.o	$$⊢\underset{\dot{}}{0}=0_D$$
4		ldualv0cl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
6		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
7		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
8	5 6 7 2 3 4	ldual0v	$$⊢\phi \to \underset{\dot{}}{0}={\mathrm{Base}}_W\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}$$
9	6 7 5 1	lfl0f	$$⊢W\in \mathrm{LMod}\to {\mathrm{Base}}_W\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\in F$$
10	4 9	syl	$$⊢\phi \to {\mathrm{Base}}_W\times \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\in F$$
11	8 10	eqeltrd	$$⊢\phi \to \underset{\dot{}}{0}\in F$$