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 = ( LFnl ` W )
	ldualelvbase.d	|- D = ( LDual ` W )
	ldualelvbase.v	|- V = ( Base ` D )
	ldualelvbase.w	|- ( ph -> W e. X )
	ldualelvbase.g	|- ( ph -> G e. F )
Assertion	ldualelvbase	|- ( ph -> G e. V )

Proof

Step	Hyp	Ref	Expression
1		ldualelvbase.f	|- F = ( LFnl ` W )
2		ldualelvbase.d	|- D = ( LDual ` W )
3		ldualelvbase.v	|- V = ( Base ` D )
4		ldualelvbase.w	|- ( ph -> W e. X )
5		ldualelvbase.g	|- ( ph -> G e. F )
6	1 2 3 4	ldualvbase	|- ( ph -> V = F )
7	5 6	eleqtrrd	|- ( ph -> G e. V )