Theorem cldcss

Description: Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015)

	Ref	Expression
Hypotheses	cldcss.v	|- V = ( Base ` W )
	cldcss.j	|- J = ( TopOpen ` W )
	cldcss.l	|- L = ( LSubSp ` W )
	cldcss.c	|- C = ( ClSubSp ` W )
Assertion	cldcss	|- ( W e. CHil -> ( U e. C <-> ( U e. L /\ U e. ( Clsd ` J ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cldcss.v	|- V = ( Base ` W )
2		cldcss.j	|- J = ( TopOpen ` W )
3		cldcss.l	|- L = ( LSubSp ` W )
4		cldcss.c	|- C = ( ClSubSp ` W )
5		hlphl	|- ( W e. CHil -> W e. PreHil )
6	4 3	csslss	|- ( ( W e. PreHil /\ U e. C ) -> U e. L )
7	5 6	sylan	|- ( ( W e. CHil /\ U e. C ) -> U e. L )
8		hlcph	|- ( W e. CHil -> W e. CPreHil )
9	4 2	csscld	|- ( ( W e. CPreHil /\ U e. C ) -> U e. ( Clsd ` J ) )
10	8 9	sylan	|- ( ( W e. CHil /\ U e. C ) -> U e. ( Clsd ` J ) )
11	7 10	jca	|- ( ( W e. CHil /\ U e. C ) -> ( U e. L /\ U e. ( Clsd ` J ) ) )
12	5	3ad2ant1	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> W e. PreHil )
13		eqid	|- ( proj ` W ) = ( proj ` W )
14	13 4	pjcss	|- ( W e. PreHil -> dom ( proj ` W ) C_ C )
15	12 14	syl	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> dom ( proj ` W ) C_ C )
16	2 3 13	pjth2	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> U e. dom ( proj ` W ) )
17	15 16	sseldd	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> U e. C )
18	17	3expb	|- ( ( W e. CHil /\ ( U e. L /\ U e. ( Clsd ` J ) ) ) -> U e. C )
19	11 18	impbida	|- ( W e. CHil -> ( U e. C <-> ( U e. L /\ U e. ( Clsd ` J ) ) ) )