Metamath Proof Explorer

Theorem cssmre

Description: The closed subspaces of a pre-Hilbert space are a Moore system. Unlike many of our other examples of closure systems, this one isnot usually an algebraic closure system df-acs : consider the Hilbert space of sequences NN --> RR with convergent sum; the subspace of all sequences with finite support is the classic example of a non-closed subspace, but for every finite set of sequences of finite support, there is a finite-dimensional (and hence closed) subspace containing all of the sequences, so if closed subspaces were an algebraic closure system this would violate acsfiel . (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses cssmre.v ⊢ V = Base W
cssmre.c ⊢ C = ClSubSp ⁡ W
Assertion cssmre ⊢ W ∈ PreHil → C ∈ Moore ⁡ V

Proof

Step Hyp Ref Expression
1 cssmre.v ⊢ V = Base W
2 cssmre.c ⊢ C = ClSubSp ⁡ W
3 1 2 cssss ⊢ x ∈ C → x ⊆ V
4 velpw ⊢ x ∈ 𝒫 V ↔ x ⊆ V
5 3 4 sylibr ⊢ x ∈ C → x ∈ 𝒫 V
6 5 a1i ⊢ W ∈ PreHil → x ∈ C → x ∈ 𝒫 V
7 6 ssrdv ⊢ W ∈ PreHil → C ⊆ 𝒫 V
8 1 2 css1 ⊢ W ∈ PreHil → V ∈ C
9 intss1 ⊢ z ∈ x → ⋂ x ⊆ z
10 eqid ⊢ ocv ⁡ W = ocv ⁡ W
11 10 ocv2ss ⊢ ⋂ x ⊆ z → ocv ⁡ W ⁡ z ⊆ ocv ⁡ W ⁡ ⋂ x
12 10 ocv2ss ⊢ ocv ⁡ W ⁡ z ⊆ ocv ⁡ W ⁡ ⋂ x → ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ⊆ ocv ⁡ W ⁡ ocv ⁡ W ⁡ z
13 9 11 12 3syl ⊢ z ∈ x → ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ⊆ ocv ⁡ W ⁡ ocv ⁡ W ⁡ z
14 13 ad2antll ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ∧ z ∈ x → ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ⊆ ocv ⁡ W ⁡ ocv ⁡ W ⁡ z
15 simprl ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ∧ z ∈ x → y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x
16 14 15 sseldd ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ∧ z ∈ x → y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ z
17 simpl2 ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ∧ z ∈ x → x ⊆ C
18 simprr ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ∧ z ∈ x → z ∈ x
19 17 18 sseldd ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ∧ z ∈ x → z ∈ C
20 10 2 cssi ⊢ z ∈ C → z = ocv ⁡ W ⁡ ocv ⁡ W ⁡ z
21 19 20 syl ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ∧ z ∈ x → z = ocv ⁡ W ⁡ ocv ⁡ W ⁡ z
22 16 21 eleqtrrd ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ∧ z ∈ x → y ∈ z
23 22 expr ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x → z ∈ x → y ∈ z
24 23 alrimiv ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x → ∀ z z ∈ x → y ∈ z
25 vex ⊢ y ∈ V
26 25 elint ⊢ y ∈ ⋂ x ↔ ∀ z z ∈ x → y ∈ z
27 24 26 sylibr ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ ∧ y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x → y ∈ ⋂ x
28 27 ex ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → y ∈ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x → y ∈ ⋂ x
29 28 ssrdv ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ⊆ ⋂ x
30 simp1 ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → W ∈ PreHil
31 intssuni ⊢ x ≠ ∅ → ⋂ x ⊆ ⋃ x
32 31 3ad2ant3 ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → ⋂ x ⊆ ⋃ x
33 simp2 ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → x ⊆ C
34 7 3ad2ant1 ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → C ⊆ 𝒫 V
35 33 34 sstrd ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → x ⊆ 𝒫 V
36 sspwuni ⊢ x ⊆ 𝒫 V ↔ ⋃ x ⊆ V
37 35 36 sylib ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → ⋃ x ⊆ V
38 32 37 sstrd ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → ⋂ x ⊆ V
39 1 2 10 iscss2 ⊢ W ∈ PreHil ∧ ⋂ x ⊆ V → ⋂ x ∈ C ↔ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ⊆ ⋂ x
40 30 38 39 syl2anc ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → ⋂ x ∈ C ↔ ocv ⁡ W ⁡ ocv ⁡ W ⁡ ⋂ x ⊆ ⋂ x
41 29 40 mpbird ⊢ W ∈ PreHil ∧ x ⊆ C ∧ x ≠ ∅ → ⋂ x ∈ C
42 7 8 41 ismred ⊢ W ∈ PreHil → C ∈ Moore ⁡ V