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