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

Metamath Proof Explorer

Theorem ldualvsval

Description: Value of scalar product operation value for the dual of a vector space. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses ldualfvs.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
ldualfvs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ldualfvs.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
ldualfvs.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
ldualfvs.t ⊢ × = ( .r ‘ 𝑅 )
ldualfvs.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualfvs.s ⊢ ∙ = ( ·𝑠 ‘ 𝐷 )
ldualfvs.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑌 )
ldualvs.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
ldualvs.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
ldualvs.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion ldualvsval ( 𝜑 → ( ( 𝑋 ∙ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) × 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ldualfvs.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 ldualfvs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 ldualfvs.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
4 ldualfvs.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
5 ldualfvs.t ⊢ × = ( .r ‘ 𝑅 )
6 ldualfvs.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
7 ldualfvs.s ⊢ ∙ = ( ·𝑠 ‘ 𝐷 )
8 ldualfvs.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑌 )
9 ldualvs.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
10 ldualvs.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
11 ldualvs.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
12 1 2 3 4 5 6 7 8 9 10 ldualvs ⊢ ( 𝜑 → ( 𝑋 ∙ 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )
13 12 fveq1d ⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) ‘ 𝐴 ) )
14 2 fvexi ⊢ 𝑉 ∈ V
15 14 a1i ⊢ ( 𝜑 → 𝑉 ∈ V )
16 3 4 2 1 lflf ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
17 8 10 16 syl2anc ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
18 17 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑉 )
19 eqidd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )
20 15 9 18 19 ofc2 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) × 𝑋 ) )
21 11 20 mpdan ⊢ ( 𝜑 → ( ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) × 𝑋 ) )
22 13 21 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 ∙ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) × 𝑋 ) )