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	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualelvbase.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualelvbase.v	$$⊢V={\mathrm{Base}}_D$$
	ldualelvbase.w	$$⊢\phi \to W\in X$$
	ldualelvbase.g	$$⊢\phi \to G\in F$$
Assertion	ldualelvbase	$$⊢\phi \to G\in V$$

Proof

Step	Hyp	Ref	Expression
1		ldualelvbase.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualelvbase.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
3		ldualelvbase.v	$$⊢V={\mathrm{Base}}_D$$
4		ldualelvbase.w	$$⊢\phi \to W\in X$$
5		ldualelvbase.g	$$⊢\phi \to G\in F$$
6	1 2 3 4	ldualvbase	$$⊢\phi \to V=F$$
7	5 6	eleqtrrd	$$⊢\phi \to G\in V$$