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 )