Theorem cphssphl

Description: A Banach subspace of a subcomplex pre-Hilbert space is a subcomplex Hilbert space. (Contributed by NM, 11-Apr-2008) (Revised by AV, 25-Sep-2022)

	Ref	Expression
Hypotheses	cphssphl.x	|- X = ( W |`s U )
	cphssphl.s	|- S = ( LSubSp ` W )
Assertion	cphssphl	|- ( ( W e. CPreHil /\ U e. S /\ X e. Ban ) -> X e. CHil )

Proof

Step	Hyp	Ref	Expression
1		cphssphl.x	|- X = ( W |`s U )
2		cphssphl.s	|- S = ( LSubSp ` W )
3		simp3	|- ( ( W e. CPreHil /\ U e. S /\ X e. Ban ) -> X e. Ban )
4	1 2	cphsscph	|- ( ( W e. CPreHil /\ U e. S ) -> X e. CPreHil )
5	4	3adant3	|- ( ( W e. CPreHil /\ U e. S /\ X e. Ban ) -> X e. CPreHil )
6		ishl	|- ( X e. CHil <-> ( X e. Ban /\ X e. CPreHil ) )
7	3 5 6	sylanbrc	|- ( ( W e. CPreHil /\ U e. S /\ X e. Ban ) -> X e. CHil )