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

Metamath Proof Explorer

Theorem ldualvs

Description: Scalar product operation value (which is a functional) 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 ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion ldualvs ( 𝜑 → ( 𝑋 ∙ 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )

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 eqid ⊢ ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) )
12 1 2 3 4 5 6 7 8 11 ldualfvs ⊢ ( 𝜑 → ∙ = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) )
13 12 oveqd ⊢ ( 𝜑 → ( 𝑋 ∙ 𝐺 ) = ( 𝑋 ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) 𝐺 ) )
14 sneq ⊢ ( 𝑘 = 𝑋 → { 𝑘 } = { 𝑋 } )
15 14 xpeq2d ⊢ ( 𝑘 = 𝑋 → ( 𝑉 × { 𝑘 } ) = ( 𝑉 × { 𝑋 } ) )
16 15 oveq2d ⊢ ( 𝑘 = 𝑋 → ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) = ( 𝑓 ∘f × ( 𝑉 × { 𝑋 } ) ) )
17 oveq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 ∘f × ( 𝑉 × { 𝑋 } ) ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )
18 ovex ⊢ ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) ∈ V
19 16 17 11 18 ovmpo ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝐺 ∈ 𝐹 ) → ( 𝑋 ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )
20 9 10 19 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )
21 13 20 eqtrd ⊢ ( 𝜑 → ( 𝑋 ∙ 𝐺 ) = ( 𝐺 ∘f × ( 𝑉 × { 𝑋 } ) ) )