Theorem ldualvscl

Description: The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Hypotheses	ldualvscl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvscl.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualvscl.k	$$⊢K={\mathrm{Base}}_R$$
	ldualvscl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvscl.s	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	ldualvscl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualvscl.x	$$⊢\phi \to X\in K$$
	ldualvscl.g	$$⊢\phi \to G\in F$$
Assertion	ldualvscl	$$⊢\phi \to X\underset{\dot{}}{·}G\in F$$

Proof

Step	Hyp	Ref	Expression
1		ldualvscl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualvscl.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		ldualvscl.k	$$⊢K={\mathrm{Base}}_R$$
4		ldualvscl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
5		ldualvscl.s	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
6		ldualvscl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		ldualvscl.x	$$⊢\phi \to X\in K$$
8		ldualvscl.g	$$⊢\phi \to G\in F$$
9		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
10		eqid	$$⊢{\cdot }_R={\cdot }_R$$
11	1 9 2 3 10 4 5 6 7 8	ldualvs	$$⊢\phi \to X\underset{\dot{}}{·}G=G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)$$
12	9 2 3 10 1 6 8 7	lflvscl	$$⊢\phi \to G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)\in F$$
13	11 12	eqeltrd	$$⊢\phi \to X\underset{\dot{}}{·}G\in F$$