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

Metamath Proof Explorer

Theorem ldualfvs

Description: Scalar product operation 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 ⊢ ( 𝜑 → 𝑊 ∈ 𝑌 )
ldualfvs.m ⊢ · = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) )
Assertion ldualfvs ( 𝜑 → ∙ = · )

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 ldualfvs.m ⊢ · = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) )
10 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
11 eqid ⊢ ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) = ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) )
12 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
13 eqid ⊢ ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) )
14 2 10 11 1 6 3 4 5 12 13 8 ldualset ⊢ ( 𝜑 → 𝐷 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) )
15 14 fveq2d ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) ) )
16 4 fvexi ⊢ 𝐾 ∈ V
17 1 fvexi ⊢ 𝐹 ∈ V
18 16 17 mpoex ⊢ ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ∈ V
19 eqid ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } )
20 19 lmodvsca ⊢ ( ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ∈ V → ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) ) )
21 18 20 ax-mp ⊢ ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) )
22 9 21 eqtri ⊢ · = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) )
23 15 7 22 3eqtr4g ⊢ ( 𝜑 → ∙ = · )