# Metamath Proof Explorer

## Theorem hhshsslem2

Description: Lemma for hhsssh . (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsst.1
`|- U = <. <. +h , .h >. , normh >.`
hhsst.2
`|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
hhssp3.3
`|- W e. ( SubSp ` U )`
hhssp3.4
`|- H C_ ~H`
Assertion hhshsslem2
`|- H e. SH`

### Proof

Step Hyp Ref Expression
1 hhsst.1
` |-  U = <. <. +h , .h >. , normh >.`
2 hhsst.2
` |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.`
3 hhssp3.3
` |-  W e. ( SubSp ` U )`
4 hhssp3.4
` |-  H C_ ~H`
5 1 hhnv
` |-  U e. NrmCVec`
6 1 hh0v
` |-  0h = ( 0vec ` U )`
7 eqid
` |-  ( 0vec ` W ) = ( 0vec ` W )`
8 eqid
` |-  ( SubSp ` U ) = ( SubSp ` U )`
9 6 7 8 sspz
` |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> ( 0vec ` W ) = 0h )`
10 5 3 9 mp2an
` |-  ( 0vec ` W ) = 0h`
11 8 sspnv
` |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> W e. NrmCVec )`
12 5 3 11 mp2an
` |-  W e. NrmCVec`
13 eqid
` |-  ( BaseSet ` W ) = ( BaseSet ` W )`
14 13 7 nvzcl
` |-  ( W e. NrmCVec -> ( 0vec ` W ) e. ( BaseSet ` W ) )`
15 12 14 ax-mp
` |-  ( 0vec ` W ) e. ( BaseSet ` W )`
16 1 2 3 4 hhshsslem1
` |-  H = ( BaseSet ` W )`
17 15 16 eleqtrri
` |-  ( 0vec ` W ) e. H`
18 10 17 eqeltrri
` |-  0h e. H`
19 4 18 pm3.2i
` |-  ( H C_ ~H /\ 0h e. H )`
20 1 hhva
` |-  +h = ( +v ` U )`
21 eqid
` |-  ( +v ` W ) = ( +v ` W )`
22 16 20 21 8 sspgval
` |-  ( ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) /\ ( x e. H /\ y e. H ) ) -> ( x ( +v ` W ) y ) = ( x +h y ) )`
23 5 3 22 mpanl12
` |-  ( ( x e. H /\ y e. H ) -> ( x ( +v ` W ) y ) = ( x +h y ) )`
24 16 21 nvgcl
` |-  ( ( W e. NrmCVec /\ x e. H /\ y e. H ) -> ( x ( +v ` W ) y ) e. H )`
25 12 24 mp3an1
` |-  ( ( x e. H /\ y e. H ) -> ( x ( +v ` W ) y ) e. H )`
26 23 25 eqeltrrd
` |-  ( ( x e. H /\ y e. H ) -> ( x +h y ) e. H )`
27 26 rgen2
` |-  A. x e. H A. y e. H ( x +h y ) e. H`
28 1 hhsm
` |-  .h = ( .sOLD ` U )`
29 eqid
` |-  ( .sOLD ` W ) = ( .sOLD ` W )`
30 16 28 29 8 sspsval
` |-  ( ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) /\ ( x e. CC /\ y e. H ) ) -> ( x ( .sOLD ` W ) y ) = ( x .h y ) )`
31 5 3 30 mpanl12
` |-  ( ( x e. CC /\ y e. H ) -> ( x ( .sOLD ` W ) y ) = ( x .h y ) )`
32 16 29 nvscl
` |-  ( ( W e. NrmCVec /\ x e. CC /\ y e. H ) -> ( x ( .sOLD ` W ) y ) e. H )`
33 12 32 mp3an1
` |-  ( ( x e. CC /\ y e. H ) -> ( x ( .sOLD ` W ) y ) e. H )`
34 31 33 eqeltrrd
` |-  ( ( x e. CC /\ y e. H ) -> ( x .h y ) e. H )`
35 34 rgen2
` |-  A. x e. CC A. y e. H ( x .h y ) e. H`
36 27 35 pm3.2i
` |-  ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H )`
37 issh2
` |-  ( H e. SH <-> ( ( H C_ ~H /\ 0h e. H ) /\ ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) )`
38 19 36 37 mpbir2an
` |-  H e. SH`