Theorem 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	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ Hil )

Proof

Step	Hyp	Ref	Expression
1		hlphl	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ PreHil )
2		eqid	⊢ ( proj ‘ 𝑊 ) = ( proj ‘ 𝑊 )
3		eqid	⊢ ( ClSubSp ‘ 𝑊 ) = ( ClSubSp ‘ 𝑊 )
4	2 3	pjcss	⊢ ( 𝑊 ∈ PreHil → dom ( proj ‘ 𝑊 ) ⊆ ( ClSubSp ‘ 𝑊 ) )
5	1 4	syl	⊢ ( 𝑊 ∈ ℂHil → dom ( proj ‘ 𝑊 ) ⊆ ( ClSubSp ‘ 𝑊 ) )
6		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7		eqid	⊢ ( TopOpen ‘ 𝑊 ) = ( TopOpen ‘ 𝑊 )
8		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9	6 7 8 3	cldcss2	⊢ ( 𝑊 ∈ ℂHil → ( ClSubSp ‘ 𝑊 ) = ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) )
10		elin	⊢ ( 𝑥 ∈ ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ↔ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑥 ∈ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) )
11	7 8 2	pjth2	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑥 ∈ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) → 𝑥 ∈ dom ( proj ‘ 𝑊 ) )
12	11	3expib	⊢ ( 𝑊 ∈ ℂHil → ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑥 ∈ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) → 𝑥 ∈ dom ( proj ‘ 𝑊 ) ) )
13	10 12	syl5bi	⊢ ( 𝑊 ∈ ℂHil → ( 𝑥 ∈ ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) → 𝑥 ∈ dom ( proj ‘ 𝑊 ) ) )
14	13	ssrdv	⊢ ( 𝑊 ∈ ℂHil → ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ⊆ dom ( proj ‘ 𝑊 ) )
15	9 14	eqsstrd	⊢ ( 𝑊 ∈ ℂHil → ( ClSubSp ‘ 𝑊 ) ⊆ dom ( proj ‘ 𝑊 ) )
16	5 15	eqssd	⊢ ( 𝑊 ∈ ℂHil → dom ( proj ‘ 𝑊 ) = ( ClSubSp ‘ 𝑊 ) )
17	2 3	ishil	⊢ ( 𝑊 ∈ Hil ↔ ( 𝑊 ∈ PreHil ∧ dom ( proj ‘ 𝑊 ) = ( ClSubSp ‘ 𝑊 ) ) )
18	1 16 17	sylanbrc	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ Hil )