Theorem pjth2

Description: Projection Theorem with abbreviations: A topologically closed subspace is a projection subspace. (Contributed by Mario Carneiro, 17-Oct-2015)

	Ref	Expression
Hypotheses	pjth2.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	pjth2.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
	pjth2.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
Assertion	pjth2	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ∈ dom 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		pjth2.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
2		pjth2.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
3		pjth2.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
4		simp2	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ∈ 𝐿 )
5		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6		eqid	⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
7		eqid	⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
8	5 6 7 1 2	pjth	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑈 ) ) = ( Base ‘ 𝑊 ) )
9		hlphl	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ PreHil )
10	9	3ad2ant1	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑊 ∈ PreHil )
11	5 2 7 6 3	pjdm2	⊢ ( 𝑊 ∈ PreHil → ( 𝑈 ∈ dom 𝐾 ↔ ( 𝑈 ∈ 𝐿 ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑈 ) ) = ( Base ‘ 𝑊 ) ) ) )
12	10 11	syl	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈 ∈ dom 𝐾 ↔ ( 𝑈 ∈ 𝐿 ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑈 ) ) = ( Base ‘ 𝑊 ) ) ) )
13	4 8 12	mpbir2and	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ∈ dom 𝐾 )