hlhil

Description: Corollary of the Projection Theorem: A subcomplex Hilbert space is a Hilbert space (in the algebraic sense, meaning that all algebraically closed subspaces have a projection decomposition). (Contributed by Mario Carneiro, 17-Oct-2015)

		Ref	Expression
	Assertion	hlhil	$⊢ W \in ℂHil \to W \in Hil$

Proof

Step	Hyp	Ref	Expression
1		hlphl	$⊢ W \in ℂHil \to W \in PreHil$
2		eqid	$⊢ proj (W) = proj (W)$
3		eqid	$⊢ ClSubSp (W) = ClSubSp (W)$
4	2 3	pjcss	$⊢ W \in PreHil \to dom proj (W) \subseteq ClSubSp (W)$
5	1 4	syl	$⊢ W \in ℂHil \to dom proj (W) \subseteq ClSubSp (W)$
6		eqid	$⊢ {Base}_{W} = {Base}_{W}$
7		eqid	$⊢ TopOpen (W) = TopOpen (W)$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9	6 7 8 3	cldcss2	$⊢ W \in ℂHil \to ClSubSp (W) = LSubSp (W) \cap Clsd (TopOpen (W))$
10		elin	$⊢ x \in (LSubSp (W) \cap Clsd (TopOpen (W))) \leftrightarrow (x \in LSubSp (W) \land x \in Clsd (TopOpen (W)))$
11	7 8 2	pjth2	$⊢ (W \in ℂHil \land x \in LSubSp (W) \land x \in Clsd (TopOpen (W))) \to x \in dom proj (W)$
12	11	3expib	$⊢ W \in ℂHil \to ((x \in LSubSp (W) \land x \in Clsd (TopOpen (W))) \to x \in dom proj (W))$
13	10 12	biimtrid	$⊢ W \in ℂHil \to (x \in (LSubSp (W) \cap Clsd (TopOpen (W))) \to x \in dom proj (W))$
14	13	ssrdv	$⊢ W \in ℂHil \to LSubSp (W) \cap Clsd (TopOpen (W)) \subseteq dom proj (W)$
15	9 14	eqsstrd	$⊢ W \in ℂHil \to ClSubSp (W) \subseteq dom proj (W)$
16	5 15	eqssd	$⊢ W \in ℂHil \to dom proj (W) = ClSubSp (W)$
17	2 3	ishil	$⊢ W \in Hil \leftrightarrow (W \in PreHil \land dom proj (W) = ClSubSp (W))$
18	1 16 17	sylanbrc	$⊢ W \in ℂHil \to W \in Hil$

Metamath Proof Explorer

Theorem hlhil

Proof