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 ) )