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 )