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	⊢ ( 𝜑 → 𝑉 = 𝐹 )