This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )
14 13 ad2antll 
 |-  ( ( ( 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 )
32 31 3ad2ant3 
 |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> |^| x C_ U. x )
33 simp2 
 |-  ( ( W e. PreHil /\ x C_ C /\ x =/= (/) ) -> x C_ C )
34 7 3ad2ant1 
 |-  ( ( 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 ) )