Metamath Proof Explorer

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 ↾_{𝑠} U$
		cphssphl.s	$⊢ S = LSubSp (W)$
	Assertion	cphssphl	$⊢ (W \in CPreHil \land U \in S \land X \in Ban) \to X \in ℂHil$

Proof

Step	Hyp	Ref	Expression
1		cphssphl.x	$⊢ X = W ↾_{𝑠} U$
2		cphssphl.s	$⊢ S = LSubSp (W)$
3		simp3	$⊢ (W \in CPreHil \land U \in S \land X \in Ban) \to X \in Ban$
4	1 2	cphsscph	$⊢ (W \in CPreHil \land U \in S) \to X \in CPreHil$
5	4	3adant3	$⊢ (W \in CPreHil \land U \in S \land X \in Ban) \to X \in CPreHil$
6		ishl	$⊢ X \in ℂHil \leftrightarrow (X \in Ban \land X \in CPreHil)$
7	3 5 6	sylanbrc	$⊢ (W \in CPreHil \land U \in S \land X \in Ban) \to X \in ℂHil$