Theorem ldualvscl

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

	Ref	Expression
Hypotheses	ldualvscl.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldualvscl.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldualvscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	ldualvscl.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualvscl.s	⊢ · = ( ·𝑠 ‘ 𝐷 )
	ldualvscl.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	ldualvscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
	ldualvscl.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	ldualvscl	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		ldualvscl.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldualvscl.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		ldualvscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		ldualvscl.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
5		ldualvscl.s	⊢ · = ( ·𝑠 ‘ 𝐷 )
6		ldualvscl.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
7		ldualvscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
8		ldualvscl.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11	1 9 2 3 10 4 5 6 7 8	ldualvs	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) = ( 𝐺 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) )
12	9 2 3 10 1 6 8 7	lflvscl	⊢ ( 𝜑 → ( 𝐺 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑋 } ) ) ∈ 𝐹 )
13	11 12	eqeltrd	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐹 )