# 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 ‘ 𝑉 ) )