Theorem lcdvscl

Description: The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015)

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

Proof

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