ldualvscl

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

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

Metamath Proof Explorer