# 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 e. PreHil -> C e. ( Moore ` V ) )`

### Proof

Step Hyp Ref Expression
1 cssmre.v
` |-  V = ( Base ` W )`
2 cssmre.c
` |-  C = ( ClSubSp ` W )`
3 1 2 cssss
` |-  ( x e. C -> x C_ V )`
4 velpw
` |-  ( x e. ~P V <-> x C_ V )`
5 3 4 sylibr
` |-  ( x e. C -> x e. ~P V )`
6 5 a1i
` |-  ( W e. PreHil -> ( x e. C -> x e. ~P V ) )`
7 6 ssrdv
` |-  ( W e. PreHil -> C C_ ~P V )`
8 1 2 css1
` |-  ( W e. PreHil -> V e. C )`
9 intss1
` |-  ( z e. x -> |^| x C_ z )`
10 eqid
` |-  ( ocv ` W ) = ( ocv ` W )`
11 10 ocv2ss
` |-  ( |^| x C_ z -> ( ( ocv ` W ) ` z ) C_ ( ( ocv ` W ) ` |^| x ) )`
12 10 ocv2ss
` |-  ( ( ( ocv ` W ) ` z ) C_ ( ( ocv ` W ) ` |^| x ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) C_ ( ( ocv ` W ) ` ( ( ocv ` W ) ` z ) ) )`
13 9 11 12 3syl
` |-  ( z e. x -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) C_ ( ( ocv ` W ) ` ( ( ocv ` W ) ` z ) ) )`
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ ( y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) /\ z e. x ) ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) C_ ( ( ocv ` W ) ` ( ( ocv ` W ) ` z ) ) )`
15 simprl
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ ( y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) /\ z e. x ) ) -> y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) )`
16 14 15 sseldd
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ ( y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) /\ z e. x ) ) -> y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` z ) ) )`
17 simpl2
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ ( y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) /\ z e. x ) ) -> x C_ C )`
18 simprr
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ ( y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) /\ z e. x ) ) -> z e. x )`
19 17 18 sseldd
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ ( y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) /\ z e. x ) ) -> z e. C )`
20 10 2 cssi
` |-  ( z e. C -> z = ( ( ocv ` W ) ` ( ( ocv ` W ) ` z ) ) )`
21 19 20 syl
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ ( y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) /\ z e. x ) ) -> z = ( ( ocv ` W ) ` ( ( ocv ` W ) ` z ) ) )`
22 16 21 eleqtrrd
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ ( y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) /\ z e. x ) ) -> y e. z )`
23 22 expr
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) ) -> ( z e. x -> y e. z ) )`
24 23 alrimiv
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) ) -> A. z ( z e. x -> y e. z ) )`
25 vex
` |-  y e. _V`
26 25 elint
` |-  ( y e. |^| x <-> A. z ( z e. x -> y e. z ) )`
27 24 26 sylibr
` |-  ( ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) /\ y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) ) -> y e. |^| x )`
28 27 ex
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> ( y e. ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) -> y e. |^| x ) )`
29 28 ssrdv
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) C_ |^| x )`
30 simp1
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> W e. PreHil )`
31 intssuni
` |-  ( x =/= (/) -> |^| x C_ U. x )`
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> |^| x C_ U. x )`
33 simp2
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> x C_ C )`
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> C C_ ~P V )`
35 33 34 sstrd
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> x C_ ~P V )`
36 sspwuni
` |-  ( x C_ ~P V <-> U. x C_ V )`
37 35 36 sylib
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> U. x C_ V )`
38 32 37 sstrd
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> |^| x C_ V )`
39 1 2 10 iscss2
` |-  ( ( W e. PreHil /\ |^| x C_ V ) -> ( |^| x e. C <-> ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) C_ |^| x ) )`
40 30 38 39 syl2anc
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> ( |^| x e. C <-> ( ( ocv ` W ) ` ( ( ocv ` W ) ` |^| x ) ) C_ |^| x ) )`
41 29 40 mpbird
` |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> |^| x e. C )`
42 7 8 41 ismred
` |-  ( W e. PreHil -> C e. ( Moore ` V ) )`