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

Metamath Proof Explorer

Theorem diassdvaN

Description: The partial isomorphism A maps to a set of vectors in partial vector space A. (Contributed by NM, 1-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses diassdva.b 
|- B = ( Base ` K )
diassdva.l 
|- .<_ = ( le ` K )
diassdva.h 
|- H = ( LHyp ` K )
diassdva.i 
|- I = ( ( DIsoA ` K ) ` W )
diassdva.u 
|- U = ( ( DVecA ` K ) ` W )
diassdva.v 
|- V = ( Base ` U )
Assertion diassdvaN 
|- ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ V )

Proof

Step Hyp Ref Expression
1 diassdva.b 
 |-  B = ( Base ` K )
2 diassdva.l 
 |-  .<_ = ( le ` K )
3 diassdva.h 
 |-  H = ( LHyp ` K )
4 diassdva.i 
 |-  I = ( ( DIsoA ` K ) ` W )
5 diassdva.u 
 |-  U = ( ( DVecA ` K ) ` W )
6 diassdva.v 
 |-  V = ( Base ` U )
7 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
8 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
9 1 2 3 7 8 4 diaval 
 |-  ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } )
10 ssrab2 
 |-  { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } C_ ( ( LTrn ` K ) ` W )
11 3 7 5 6 dvavbase 
 |-  ( ( K e. Y /\ W e. H ) -> V = ( ( LTrn ` K ) ` W ) )
12 11 adantr 
 |-  ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> V = ( ( LTrn ` K ) ` W ) )
13 10 12 sseqtrrid 
 |-  ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ X } C_ V )
14 9 13 eqsstrd 
 |-  ( ( ( K e. Y /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ V )