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

Metamath Proof Explorer

Theorem dibss

Description: The partial isomorphism B maps to a set of vectors in full vector space H. (Contributed by NM, 1-Jan-2014)

Ref Expression
Hypotheses dibss.b 
|- B = ( Base ` K )
dibss.l 
|- .<_ = ( le ` K )
dibss.h 
|- H = ( LHyp ` K )
dibss.i 
|- I = ( ( DIsoB ` K ) ` W )
dibss.u 
|- U = ( ( DVecH ` K ) ` W )
dibss.v 
|- V = ( Base ` U )
Assertion dibss 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ V )

Proof

Step Hyp Ref Expression
1 dibss.b 
 |-  B = ( Base ` K )
2 dibss.l 
 |-  .<_ = ( le ` K )
3 dibss.h 
 |-  H = ( LHyp ` K )
4 dibss.i 
 |-  I = ( ( DIsoB ` K ) ` W )
5 dibss.u 
 |-  U = ( ( DVecH ` K ) ` W )
6 dibss.v 
 |-  V = ( Base ` U )
7 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
8 eqid 
 |-  ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
9 1 2 3 7 8 diass 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( ( DIsoA ` K ) ` W ) ` X ) C_ ( ( LTrn ` K ) ` W ) )
10 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
11 eqid 
 |-  ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) )
12 1 3 7 10 11 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) e. ( ( TEndo ` K ) ` W ) )
13 12 snssd 
 |-  ( ( K e. HL /\ W e. H ) -> { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } C_ ( ( TEndo ` K ) ` W ) )
14 13 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } C_ ( ( TEndo ` K ) ` W ) )
15 xpss12 
 |-  ( ( ( ( ( DIsoA ` K ) ` W ) ` X ) C_ ( ( LTrn ` K ) ` W ) /\ { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } C_ ( ( TEndo ` K ) ` W ) ) -> ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
16 9 14 15 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
17 1 2 3 7 11 8 4 dibval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) )
18 3 7 10 5 6 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> V = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
19 18 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> V = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
20 16 17 19 3sstr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) C_ V )