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

Metamath Proof Explorer

Theorem ldualfvadd

Description: Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses ldualvadd.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
ldualvadd.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
ldualvadd.a ⊢ + = ( +g ‘ 𝑅 )
ldualvadd.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualvadd.p ⊢ ✚ = ( +g ‘ 𝐷 )
ldualvadd.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
ldualfvadd.q ⊢ ⨣ = ( ∘f + ↾ ( 𝐹 × 𝐹 ) )
Assertion ldualfvadd ( 𝜑 → ✚ = ⨣ )

Proof

Step Hyp Ref Expression
1 ldualvadd.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 ldualvadd.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3 ldualvadd.a ⊢ + = ( +g ‘ 𝑅 )
4 ldualvadd.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
5 ldualvadd.p ⊢ ✚ = ( +g ‘ 𝐷 )
6 ldualvadd.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
7 ldualfvadd.q ⊢ ⨣ = ( ∘f + ↾ ( 𝐹 × 𝐹 ) )
8 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
12 eqid ⊢ ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) = ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) )
13 8 3 7 1 4 2 9 10 11 12 6 ldualset ⊢ ( 𝜑 → 𝐷 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) )
14 13 fveq2d ⊢ ( 𝜑 → ( +g ‘ 𝐷 ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) ) )
15 1 fvexi ⊢ 𝐹 ∈ V
16 id ⊢ ( 𝐹 ∈ V → 𝐹 ∈ V )
17 16 16 ofmresex ⊢ ( 𝐹 ∈ V → ( ∘f + ↾ ( 𝐹 × 𝐹 ) ) ∈ V )
18 15 17 ax-mp ⊢ ( ∘f + ↾ ( 𝐹 × 𝐹 ) ) ∈ V
19 7 18 eqeltri ⊢ ⨣ ∈ V
20 eqid ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } )
21 20 lmodplusg ⊢ ( ⨣ ∈ V → ⨣ = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) ) )
22 19 21 ax-mp ⊢ ⨣ = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) )
23 14 5 22 3eqtr4g ⊢ ( 𝜑 → ✚ = ⨣ )