Theorem hhsssh2

Description: The predicate " H is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhsssh2.1	|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
Assertion	hhsssh2	|- ( H e. SH <-> ( W e. NrmCVec /\ H C_ ~H ) )

Proof

Step	Hyp	Ref	Expression
1		hhsssh2.1	|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
2		eqid	|- <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
3	2 1	hhsssh	|- ( H e. SH <-> ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) /\ H C_ ~H ) )
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	2	hhnv	|- <. <. +h , .h >. , normh >. e. NrmCVec
9	2	hhva	|- +h = ( +v ` <. <. +h , .h >. , normh >. )
10	1	hhssva	|- ( +h |` ( H X. H ) ) = ( +v ` W )
11	2	hhsm	|- .h = ( .sOLD ` <. <. +h , .h >. , normh >. )
12	1	hhsssm	|- ( .h |` ( CC X. H ) ) = ( .sOLD ` W )
13	2	hhnm	|- normh = ( normCV ` <. <. +h , .h >. , normh >. )
14	1	hhssnm	|- ( normh |` H ) = ( normCV ` W )
15		eqid	|- ( SubSp ` <. <. +h , .h >. , normh >. ) = ( SubSp ` <. <. +h , .h >. , normh >. )
16	9 10 11 12 13 14 15	isssp	|- ( <. <. +h , .h >. , normh >. e. NrmCVec -> ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) <-> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) ) )
17	8 16	ax-mp	|- ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) <-> ( W e. NrmCVec /\ ( ( +h |` ( H X. H ) ) C_ +h /\ ( .h |` ( CC X. H ) ) C_ .h /\ ( normh |` H ) C_ normh ) ) )
18	7 17	mpbiran2	|- ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) <-> W e. NrmCVec )
19	18	anbi1i	|- ( ( W e. ( SubSp ` <. <. +h , .h >. , normh >. ) /\ H C_ ~H ) <-> ( W e. NrmCVec /\ H C_ ~H ) )
20	3 19	bitri	|- ( H e. SH <-> ( W e. NrmCVec /\ H C_ ~H ) )