This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐹 )