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 
|- 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 )