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

Metamath Proof Explorer

Theorem hhsst

Description: A member of SH is a subspace. (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 ) >.
Assertion hhsst 
|- ( H e. SH -> W e. ( SubSp ` U ) )

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 2 hhssnvt 
 |-  ( H e. SH -> W e. NrmCVec )
4 resss 
 |-  ( +h |` ( H X. H ) ) C_ +h
5 resss 
 |-  ( .h |` ( CC X. H ) ) C_ .h
6 resss 
 |-  ( normh |` H ) C_ normh
7 4 5 6 3pm3.2i 
 |-  ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh )
8 3 7 jctir 
 |-  ( H e. SH -> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) )
9 1 hhnv 
 |-  U e. NrmCVec
10 1 hhva 
 |-  +h = ( +v ` U )
11 2 hhssva 
 |-  ( +h |` ( H X. H ) ) = ( +v ` W )
12 1 hhsm 
 |-  .h = ( .sOLD ` U )
13 2 hhsssm 
 |-  ( .h |` ( CC X. H ) ) = ( .sOLD ` W )
14 1 hhnm 
 |-  normh = ( normCV ` U )
15 2 hhssnm 
 |-  ( normh |` H ) = ( normCV ` W )
16 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
17 10 11 12 13 14 15 16 isssp 
 |-  ( U e. NrmCVec -> ( W e. ( SubSp ` U ) <-> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) ) )
18 9 17 ax-mp 
 |-  ( W e. ( SubSp ` U ) <-> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) )
19 8 18 sylibr 
 |-  ( H e. SH -> W e. ( SubSp ` U ) )