Theorem pjcss

Description: A projection subspace is an (algebraically) closed subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjcss.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
	pjcss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion	pjcss	⊢ ( 𝑊 ∈ PreHil → dom 𝐾 ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		pjcss.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
2		pjcss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4		eqid	⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
5		eqid	⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
6		simpl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ dom 𝐾 ) → 𝑊 ∈ PreHil )
7		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
8	3 7 4 5 1	pjdm2	⊢ ( 𝑊 ∈ PreHil → ( 𝑥 ∈ dom 𝐾 ↔ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑥 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) = ( Base ‘ 𝑊 ) ) ) )
9	8	simprbda	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ dom 𝐾 ) → 𝑥 ∈ ( LSubSp ‘ 𝑊 ) )
10	3 7	lssss	⊢ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) → 𝑥 ⊆ ( Base ‘ 𝑊 ) )
11	9 10	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ dom 𝐾 ) → 𝑥 ⊆ ( Base ‘ 𝑊 ) )
12	3 4	ocvss	⊢ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ⊆ ( Base ‘ 𝑊 )
13	8	simplbda	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ dom 𝐾 ) → ( 𝑥 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) = ( Base ‘ 𝑊 ) )
14	12 13	sseqtrrid	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ dom 𝐾 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ⊆ ( 𝑥 ( LSSum ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) )
15	2 3 4 5 6 11 14	lsmcss	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ dom 𝐾 ) → 𝑥 ∈ 𝐶 )
16	15	ex	⊢ ( 𝑊 ∈ PreHil → ( 𝑥 ∈ dom 𝐾 → 𝑥 ∈ 𝐶 ) )
17	16	ssrdv	⊢ ( 𝑊 ∈ PreHil → dom 𝐾 ⊆ 𝐶 )