# Metamath Proof Explorer

## Theorem dihlss

Description: The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihlss.b
`|- B = ( Base ` K )`
dihlss.h
`|- H = ( LHyp ` K )`
dihlss.i
`|- I = ( ( DIsoH ` K ) ` W )`
dihlss.u
`|- U = ( ( DVecH ` K ) ` W )`
dihlss.s
`|- S = ( LSubSp ` U )`
Assertion dihlss
`|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. S )`

### Proof

Step Hyp Ref Expression
1 dihlss.b
` |-  B = ( Base ` K )`
2 dihlss.h
` |-  H = ( LHyp ` K )`
3 dihlss.i
` |-  I = ( ( DIsoH ` K ) ` W )`
4 dihlss.u
` |-  U = ( ( DVecH ` K ) ` W )`
5 dihlss.s
` |-  S = ( LSubSp ` U )`
6 eqid
` |-  ( le ` K ) = ( le ` K )`
7 eqid
` |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )`
8 1 6 2 3 7 dihvalb
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X ( le ` K ) W ) ) -> ( I ` X ) = ( ( ( DIsoB ` K ) ` W ) ` X ) )`
9 1 6 2 4 7 5 diblss
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X ( le ` K ) W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` X ) e. S )`
10 8 9 eqeltrd
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X ( le ` K ) W ) ) -> ( I ` X ) e. S )`
11 10 anassrs
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B ) /\ X ( le ` K ) W ) -> ( I ` X ) e. S )`
12 eqid
` |-  ( join ` K ) = ( join ` K )`
13 eqid
` |-  ( meet ` K ) = ( meet ` K )`
14 eqid
` |-  ( Atoms ` K ) = ( Atoms ` K )`
15 eqid
` |-  ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )`
16 eqid
` |-  ( LSSum ` U ) = ( LSSum ` U )`
17 1 6 12 13 14 2 3 7 15 4 5 16 dihlsscpre
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X ( le ` K ) W ) ) -> ( I ` X ) e. S )`
18 17 anassrs
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B ) /\ -. X ( le ` K ) W ) -> ( I ` X ) e. S )`
19 11 18 pm2.61dan
` |-  ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. S )`