Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		cmslsschl.x	$⊢ X = W ↾_{𝑠} U$
2		chlcsschl.s	$⊢ S = ClSubSp (W)$
3		hlbn	$⊢ W \in ℂHil \to W \in Ban$
4		hlcph	$⊢ W \in ℂHil \to W \in CPreHil$
5	3 4	jca	$⊢ W \in ℂHil \to (W \in Ban \land W \in CPreHil)$
6	1 2	bncssbn	$⊢ ((W \in Ban \land W \in CPreHil) \land U \in S) \to X \in Ban$
7	5 6	sylan	$⊢ (W \in ℂHil \land U \in S) \to X \in Ban$
8		hlphl	$⊢ W \in ℂHil \to W \in PreHil$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10	2 9	csslss	$⊢ (W \in PreHil \land U \in S) \to U \in LSubSp (W)$
11	8 10	sylan	$⊢ (W \in ℂHil \land U \in S) \to U \in LSubSp (W)$
12	1 9	cphsscph	$⊢ (W \in CPreHil \land U \in LSubSp (W)) \to X \in CPreHil$
13	4 11 12	syl2an2r	$⊢ (W \in ℂHil \land U \in S) \to X \in CPreHil$
14		ishl	$⊢ X \in ℂHil \leftrightarrow (X \in Ban \land X \in CPreHil)$
15	7 13 14	sylanbrc	$⊢ (W \in ℂHil \land U \in S) \to X \in ℂHil$