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

Metamath Proof Explorer

Theorem ldualvbase

Description: The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses ldualvbase.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
ldualvbase.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualvbase.v ⊢ 𝑉 = ( Base ‘ 𝐷 )
ldualvbase.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
Assertion ldualvbase ( 𝜑 → 𝑉 = 𝐹 )

Proof

Step Hyp Ref Expression
1 ldualvbase.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 ldualvbase.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
3 ldualvbase.v ⊢ 𝑉 = ( Base ‘ 𝐷 )
4 ldualvbase.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
5 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
7 eqid ⊢ ( ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( 𝐹 × 𝐹 ) ) = ( ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( 𝐹 × 𝐹 ) )
8 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
9 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
10 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
11 eqid ⊢ ( oppr ‘ ( Scalar ‘ 𝑊 ) ) = ( oppr ‘ ( Scalar ‘ 𝑊 ) )
12 eqid ⊢ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) = ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) )
13 5 6 7 1 2 8 9 10 11 12 4 ldualset ⊢ ( 𝜑 → 𝐷 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑊 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) )
14 13 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑊 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) ) )
15 1 fvexi ⊢ 𝐹 ∈ V
16 eqid ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑊 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑊 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } )
17 16 lmodbase ⊢ ( 𝐹 ∈ V → 𝐹 = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑊 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) ) )
18 15 17 ax-mp ⊢ 𝐹 = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑊 ) ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑊 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) )
19 14 3 18 3eqtr4g ⊢ ( 𝜑 → 𝑉 = 𝐹 )