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

Metamath Proof Explorer

Theorem ldualelvbase

Description: Utility theorem for converting a functional to a vector of the dual space in order to use standard vector theorems. (Contributed by NM, 6-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ldualelvbase.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldualelvbase.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
3		ldualelvbase.v	⊢ 𝑉 = ( Base ‘ 𝐷 )
4		ldualelvbase.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
5		ldualelvbase.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
6	1 2 3 4	ldualvbase	⊢ ( 𝜑 → 𝑉 = 𝐹 )
7	5 6	eleqtrrd	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )