# Metamath Proof Explorer

## Theorem diasslssN

Description: The partial isomorphism A maps to subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 diasslss.h
` |-  H = ( LHyp ` K )`
2 diasslss.u
` |-  U = ( ( DVecA ` K ) ` W )`
3 diasslss.i
` |-  I = ( ( DIsoA ` K ) ` W )`
4 diasslss.s
` |-  S = ( LSubSp ` U )`
5 1 3 diaf11N
` |-  ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )`
6 f1ocnvfv2
` |-  ( ( I : dom I -1-1-onto-> ran I /\ x e. ran I ) -> ( I ` ( `' I ` x ) ) = x )`
7 5 6 sylan
` |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> ( I ` ( `' I ` x ) ) = x )`
8 1 3 diacnvclN
` |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> ( `' I ` x ) e. dom I )`
9 eqid
` |-  ( Base ` K ) = ( Base ` K )`
10 eqid
` |-  ( le ` K ) = ( le ` K )`
11 9 10 1 3 diaeldm
` |-  ( ( K e. HL /\ W e. H ) -> ( ( `' I ` x ) e. dom I <-> ( ( `' I ` x ) e. ( Base ` K ) /\ ( `' I ` x ) ( le ` K ) W ) ) )`
` |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> ( ( `' I ` x ) e. dom I <-> ( ( `' I ` x ) e. ( Base ` K ) /\ ( `' I ` x ) ( le ` K ) W ) ) )`
13 8 12 mpbid
` |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> ( ( `' I ` x ) e. ( Base ` K ) /\ ( `' I ` x ) ( le ` K ) W ) )`
14 9 10 1 2 3 4 dialss
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( `' I ` x ) e. ( Base ` K ) /\ ( `' I ` x ) ( le ` K ) W ) ) -> ( I ` ( `' I ` x ) ) e. S )`
15 13 14 syldan
` |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> ( I ` ( `' I ` x ) ) e. S )`
16 7 15 eqeltrrd
` |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> x e. S )`
17 16 ex
` |-  ( ( K e. HL /\ W e. H ) -> ( x e. ran I -> x e. S ) )`
18 17 ssrdv
` |-  ( ( K e. HL /\ W e. H ) -> ran I C_ S )`