# 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}={\mathrm{Base}}_{{W}}$
cssmre.c ${⊢}{C}=\mathrm{ClSubSp}\left({W}\right)$
Assertion cssmre ${⊢}{W}\in \mathrm{PreHil}\to {C}\in \mathrm{Moore}\left({V}\right)$

### Proof

Step Hyp Ref Expression
1 cssmre.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 cssmre.c ${⊢}{C}=\mathrm{ClSubSp}\left({W}\right)$
3 1 2 cssss ${⊢}{x}\in {C}\to {x}\subseteq {V}$
4 velpw ${⊢}{x}\in 𝒫{V}↔{x}\subseteq {V}$
5 3 4 sylibr ${⊢}{x}\in {C}\to {x}\in 𝒫{V}$
6 5 a1i ${⊢}{W}\in \mathrm{PreHil}\to \left({x}\in {C}\to {x}\in 𝒫{V}\right)$
7 6 ssrdv ${⊢}{W}\in \mathrm{PreHil}\to {C}\subseteq 𝒫{V}$
8 1 2 css1 ${⊢}{W}\in \mathrm{PreHil}\to {V}\in {C}$
9 intss1 ${⊢}{z}\in {x}\to \bigcap {x}\subseteq {z}$
10 eqid ${⊢}\mathrm{ocv}\left({W}\right)=\mathrm{ocv}\left({W}\right)$
11 10 ocv2ss ${⊢}\bigcap {x}\subseteq {z}\to \mathrm{ocv}\left({W}\right)\left({z}\right)\subseteq \mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)$
12 10 ocv2ss ${⊢}\mathrm{ocv}\left({W}\right)\left({z}\right)\subseteq \mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\to \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\subseteq \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left({z}\right)\right)$
13 9 11 12 3syl ${⊢}{z}\in {x}\to \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\subseteq \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left({z}\right)\right)$
14 13 ad2antll ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge \left({y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\wedge {z}\in {x}\right)\right)\to \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\subseteq \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left({z}\right)\right)$
15 simprl ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge \left({y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\wedge {z}\in {x}\right)\right)\to {y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)$
16 14 15 sseldd ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge \left({y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\wedge {z}\in {x}\right)\right)\to {y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left({z}\right)\right)$
17 simpl2 ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge \left({y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\wedge {z}\in {x}\right)\right)\to {x}\subseteq {C}$
18 simprr ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge \left({y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\wedge {z}\in {x}\right)\right)\to {z}\in {x}$
19 17 18 sseldd ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge \left({y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\wedge {z}\in {x}\right)\right)\to {z}\in {C}$
20 10 2 cssi ${⊢}{z}\in {C}\to {z}=\mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left({z}\right)\right)$
21 19 20 syl ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge \left({y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\wedge {z}\in {x}\right)\right)\to {z}=\mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left({z}\right)\right)$
22 16 21 eleqtrrd ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge \left({y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\wedge {z}\in {x}\right)\right)\to {y}\in {z}$
23 22 expr ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge {y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\right)\to \left({z}\in {x}\to {y}\in {z}\right)$
24 23 alrimiv ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge {y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to {y}\in {z}\right)$
25 vex ${⊢}{y}\in \mathrm{V}$
26 25 elint ${⊢}{y}\in \bigcap {x}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}\to {y}\in {z}\right)$
27 24 26 sylibr ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\wedge {y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\right)\to {y}\in \bigcap {x}$
28 27 ex ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to \left({y}\in \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\to {y}\in \bigcap {x}\right)$
29 28 ssrdv ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\subseteq \bigcap {x}$
30 simp1 ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to {W}\in \mathrm{PreHil}$
31 intssuni ${⊢}{x}\ne \varnothing \to \bigcap {x}\subseteq \bigcup {x}$
32 31 3ad2ant3 ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to \bigcap {x}\subseteq \bigcup {x}$
33 simp2 ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to {x}\subseteq {C}$
34 7 3ad2ant1 ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to {C}\subseteq 𝒫{V}$
35 33 34 sstrd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to {x}\subseteq 𝒫{V}$
36 sspwuni ${⊢}{x}\subseteq 𝒫{V}↔\bigcup {x}\subseteq {V}$
37 35 36 sylib ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to \bigcup {x}\subseteq {V}$
38 32 37 sstrd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to \bigcap {x}\subseteq {V}$
39 1 2 10 iscss2 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \bigcap {x}\subseteq {V}\right)\to \left(\bigcap {x}\in {C}↔\mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\subseteq \bigcap {x}\right)$
40 30 38 39 syl2anc ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to \left(\bigcap {x}\in {C}↔\mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left(\bigcap {x}\right)\right)\subseteq \bigcap {x}\right)$
41 29 40 mpbird ${⊢}\left({W}\in \mathrm{PreHil}\wedge {x}\subseteq {C}\wedge {x}\ne \varnothing \right)\to \bigcap {x}\in {C}$
42 7 8 41 ismred ${⊢}{W}\in \mathrm{PreHil}\to {C}\in \mathrm{Moore}\left({V}\right)$