cmslsschl

Description: A complete linear subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by AV, 8-Oct-2022)

	Ref	Expression
Hypotheses	cmslsschl.x	$⊢ X = W ↾_{𝑠} U$
	cmslsschl.s	$⊢ S = LSubSp (W)$
Assertion	cmslsschl	$⊢ (W \in ℂHil \land X \in CMetSp \land U \in S) \to X \in ℂHil$

Step	Hyp	Ref	Expression
1		cmslsschl.x	$⊢ X = W ↾_{𝑠} U$
2		cmslsschl.s	$⊢ S = LSubSp (W)$
3		hlbn	$⊢ W \in ℂHil \to W \in Ban$
4		bnnvc	$⊢ W \in Ban \to W \in NrmVec$
5	3 4	syl	$⊢ W \in ℂHil \to W \in NrmVec$
6	5	3ad2ant1	$⊢ (W \in ℂHil \land X \in CMetSp \land U \in S) \to W \in NrmVec$
7		eqid	$⊢ Scalar (W) = Scalar (W)$
8	7	bnsca	$⊢ W \in Ban \to Scalar (W) \in CMetSp$
9	3 8	syl	$⊢ W \in ℂHil \to Scalar (W) \in CMetSp$
10	9	3ad2ant1	$⊢ (W \in ℂHil \land X \in CMetSp \land U \in S) \to Scalar (W) \in CMetSp$
11		3simpc	$⊢ (W \in ℂHil \land X \in CMetSp \land U \in S) \to (X \in CMetSp \land U \in S)$
12	1 2	cmslssbn	$⊢ ((W \in NrmVec \land Scalar (W) \in CMetSp) \land (X \in CMetSp \land U \in S)) \to X \in Ban$
13	6 10 11 12	syl21anc	$⊢ (W \in ℂHil \land X \in CMetSp \land U \in S) \to X \in Ban$
14		hlcph	$⊢ W \in ℂHil \to W \in CPreHil$
15	1 2	cphsscph	$⊢ (W \in CPreHil \land U \in S) \to X \in CPreHil$
16	14 15	sylan	$⊢ (W \in ℂHil \land U \in S) \to X \in CPreHil$
17	16	3adant2	$⊢ (W \in ℂHil \land X \in CMetSp \land U \in S) \to X \in CPreHil$
18		ishl	$⊢ X \in ℂHil \leftrightarrow (X \in Ban \land X \in CPreHil)$
19	13 17 18	sylanbrc	$⊢ (W \in ℂHil \land X \in CMetSp \land U \in S) \to X \in ℂHil$

Metamath Proof Explorer