Theorem chlcsschl

Description: A closed subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by NM, 10-Apr-2008) (Revised by AV, 8-Oct-2022)

	Ref	Expression
Hypotheses	cmslsschl.x	|- X = ( W |`s U )
	chlcsschl.s	|- S = ( ClSubSp ` W )
Assertion	chlcsschl	|- ( ( W e. CHil /\ U e. S ) -> X e. CHil )

Proof

Step	Hyp	Ref	Expression
1		cmslsschl.x	|- X = ( W |`s U )
2		chlcsschl.s	|- S = ( ClSubSp ` W )
3		hlbn	|- ( W e. CHil -> W e. Ban )
4		hlcph	|- ( W e. CHil -> W e. CPreHil )
5	3 4	jca	|- ( W e. CHil -> ( W e. Ban /\ W e. CPreHil ) )
6	1 2	bncssbn	|- ( ( ( W e. Ban /\ W e. CPreHil ) /\ U e. S ) -> X e. Ban )
7	5 6	sylan	|- ( ( W e. CHil /\ U e. S ) -> X e. Ban )
8		hlphl	|- ( W e. CHil -> W e. PreHil )
9		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
10	2 9	csslss	|- ( ( W e. PreHil /\ U e. S ) -> U e. ( LSubSp ` W ) )
11	8 10	sylan	|- ( ( W e. CHil /\ U e. S ) -> U e. ( LSubSp ` W ) )
12	1 9	cphsscph	|- ( ( W e. CPreHil /\ U e. ( LSubSp ` W ) ) -> X e. CPreHil )
13	4 11 12	syl2an2r	|- ( ( W e. CHil /\ U e. S ) -> X e. CPreHil )
14		ishl	|- ( X e. CHil <-> ( X e. Ban /\ X e. CPreHil ) )
15	7 13 14	sylanbrc	|- ( ( W e. CHil /\ U e. S ) -> X e. CHil )