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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
cssmre.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion cssmre ( 𝑊 ∈ PreHil → 𝐶 ∈ ( Moore ‘ 𝑉 ) )

Proof

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