Metamath Proof Explorer

Theorem pjcss

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

Ref Expression
Hypotheses pjcss.k ⊢ K = proj ⁡ W
pjcss.c ⊢ C = ClSubSp ⁡ W
Assertion pjcss ⊢ W ∈ PreHil → dom ⁡ K ⊆ C

Proof

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