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

Metamath Proof Explorer

Theorem dihsslss

Description: The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dihsslss.h 
|- H = ( LHyp ` K )
dihsslss.u 
|- U = ( ( DVecH ` K ) ` W )
dihsslss.i 
|- I = ( ( DIsoH ` K ) ` W )
dihsslss.s 
|- S = ( LSubSp ` U )
Assertion dihsslss 
|- ( ( K e. HL /\ W e. H ) -> ran I C_ S )

Proof

Step Hyp Ref Expression
1 dihsslss.h 
 |-  H = ( LHyp ` K )
2 dihsslss.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dihsslss.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dihsslss.s 
 |-  S = ( LSubSp ` U )
5 1 3 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> ( I ` ( `' I ` x ) ) = x )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 6 1 3 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> ( `' I ` x ) e. ( Base ` K ) )
8 6 1 3 2 4 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( `' I ` x ) e. ( Base ` K ) ) -> ( I ` ( `' I ` x ) ) e. S )
9 7 8 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> ( I ` ( `' I ` x ) ) e. S )
10 5 9 eqeltrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> x e. S )
11 10 ex 
 |-  ( ( K e. HL /\ W e. H ) -> ( x e. ran I -> x e. S ) )
12 11 ssrdv 
 |-  ( ( K e. HL /\ W e. H ) -> ran I C_ S )