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

Metamath Proof Explorer

Theorem ldualsca

Description: The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses ldualsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
ldualsca.o ⊢ 𝑂 = ( oppr ‘ 𝐹 )
ldualsca.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualsca.r ⊢ 𝑅 = ( Scalar ‘ 𝐷 )
ldualsca.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
Assertion ldualsca ( 𝜑 → 𝑅 = 𝑂 )

Proof

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