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

Metamath Proof Explorer

Theorem dvhelvbasei

Description: Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014)

Ref Expression
Hypotheses dvhvbase.h 
|- H = ( LHyp ` K )
dvhvbase.t 
|- T = ( ( LTrn ` K ) ` W )
dvhvbase.e 
|- E = ( ( TEndo ` K ) ` W )
dvhvbase.u 
|- U = ( ( DVecH ` K ) ` W )
dvhvbase.v 
|- V = ( Base ` U )
Assertion dvhelvbasei 
|- ( ( ( K e. X /\ W e. H ) /\ ( F e. T /\ S e. E ) ) -> <. F , S >. e. V )

Proof

Step Hyp Ref Expression
1 dvhvbase.h 
 |-  H = ( LHyp ` K )
2 dvhvbase.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dvhvbase.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 dvhvbase.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dvhvbase.v 
 |-  V = ( Base ` U )
6 opelxpi 
 |-  ( ( F e. T /\ S e. E ) -> <. F , S >. e. ( T X. E ) )
7 6 adantl 
 |-  ( ( ( K e. X /\ W e. H ) /\ ( F e. T /\ S e. E ) ) -> <. F , S >. e. ( T X. E ) )
8 1 2 3 4 5 dvhvbase 
 |-  ( ( K e. X /\ W e. H ) -> V = ( T X. E ) )
9 8 adantr 
 |-  ( ( ( K e. X /\ W e. H ) /\ ( F e. T /\ S e. E ) ) -> V = ( T X. E ) )
10 7 9 eleqtrrd 
 |-  ( ( ( K e. X /\ W e. H ) /\ ( F e. T /\ S e. E ) ) -> <. F , S >. e. V )