Metamath Proof Explorer

Theorem lsmcss

Description: A subset of a pre-Hilbert space whose double orthocomplement has a projection decomposition is a closed subspace. This is the core of the proof that a topologically closed subspace is algebraically closed in a Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses lsmcss.c 
|- C = ( ClSubSp ` W )
lsmcss.j 
|- V = ( Base ` W )
lsmcss.o 
|- ._|_ = ( ocv ` W )
lsmcss.p 
|- .(+) = ( LSSum ` W )
lsmcss.1 
|- ( ph -> W e. PreHil )
lsmcss.2 
|- ( ph -> S C_ V )
lsmcss.3 
|- ( ph -> ( ._|_ ` ( ._|_ ` S ) ) C_ ( S .(+) ( ._|_ ` S ) ) )
Assertion lsmcss 
|- ( ph -> S e. C )

Proof

Step Hyp Ref Expression
1 lsmcss.c 
 |-  C = ( ClSubSp ` W )
2 lsmcss.j 
 |-  V = ( Base ` W )
3 lsmcss.o 
 |-  ._|_ = ( ocv ` W )
4 lsmcss.p 
 |-  .(+) = ( LSSum ` W )
5 lsmcss.1 
 |-  ( ph -> W e. PreHil )
6 lsmcss.2 
 |-  ( ph -> S C_ V )
7 lsmcss.3 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` S ) ) C_ ( S .(+) ( ._|_ ` S ) ) )
8 7 sseld 
 |-  ( ph -> ( x e. ( ._|_ ` ( ._|_ ` S ) ) -> x e. ( S .(+) ( ._|_ ` S ) ) ) )
9 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
10 5 9 syl 
 |-  ( ph -> W e. LMod )
11 2 3 ocvss 
 |-  ( ._|_ ` S ) C_ V
12 11 a1i 
 |-  ( ph -> ( ._|_ ` S ) C_ V )
13 eqid 
 |-  ( +g ` W ) = ( +g ` W )
14 2 13 4 lsmelvalx 
 |-  ( ( W e. LMod /\ S C_ V /\ ( ._|_ ` S ) C_ V ) -> ( x e. ( S .(+) ( ._|_ ` S ) ) <-> E. y e. S E. z e. ( ._|_ ` S ) x = ( y ( +g ` W ) z ) ) )
15 10 6 12 14 syl3anc 
 |-  ( ph -> ( x e. ( S .(+) ( ._|_ ` S ) ) <-> E. y e. S E. z e. ( ._|_ ` S ) x = ( y ( +g ` W ) z ) ) )
16 8 15 sylibd 
 |-  ( ph -> ( x e. ( ._|_ ` ( ._|_ ` S ) ) -> E. y e. S E. z e. ( ._|_ ` S ) x = ( y ( +g ` W ) z ) ) )
17 5 ad2antrr 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> W e. PreHil )
18 6 ad2antrr 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> S C_ V )
19 simplrl 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> y e. S )
20 18 19 sseldd 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> y e. V )
21 simplrr 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> z e. ( ._|_ ` S ) )
22 11 21 sselid 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> z e. V )
23 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
24 eqid 
 |-  ( .i ` W ) = ( .i ` W )
25 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
26 23 24 2 13 25 ipdir 
 |-  ( ( W e. PreHil /\ ( y e. V /\ z e. V /\ z e. V ) ) -> ( ( y ( +g ` W ) z ) ( .i ` W ) z ) = ( ( y ( .i ` W ) z ) ( +g ` ( Scalar ` W ) ) ( z ( .i ` W ) z ) ) )
27 17 20 22 22 26 syl13anc 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( ( y ( +g ` W ) z ) ( .i ` W ) z ) = ( ( y ( .i ` W ) z ) ( +g ` ( Scalar ` W ) ) ( z ( .i ` W ) z ) ) )
28 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
29 2 24 23 28 3 ocvi 
 |-  ( ( z e. ( ._|_ ` S ) /\ y e. S ) -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
30 21 19 29 syl2anc 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
31 23 24 2 28 iporthcom 
 |-  ( ( W e. PreHil /\ z e. V /\ y e. V ) -> ( ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) <-> ( y ( .i ` W ) z ) = ( 0g ` ( Scalar ` W ) ) ) )
32 17 22 20 31 syl3anc 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) <-> ( y ( .i ` W ) z ) = ( 0g ` ( Scalar ` W ) ) ) )
33 30 32 mpbid 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( y ( .i ` W ) z ) = ( 0g ` ( Scalar ` W ) ) )
34 33 oveq1d 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( ( y ( .i ` W ) z ) ( +g ` ( Scalar ` W ) ) ( z ( .i ` W ) z ) ) = ( ( 0g ` ( Scalar ` W ) ) ( +g ` ( Scalar ` W ) ) ( z ( .i ` W ) z ) ) )
35 17 9 syl 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> W e. LMod )
36 23 lmodfgrp 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Grp )
37 35 36 syl 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( Scalar ` W ) e. Grp )
38 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
39 23 24 2 38 ipcl 
 |-  ( ( W e. PreHil /\ z e. V /\ z e. V ) -> ( z ( .i ` W ) z ) e. ( Base ` ( Scalar ` W ) ) )
40 17 22 22 39 syl3anc 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( z ( .i ` W ) z ) e. ( Base ` ( Scalar ` W ) ) )
41 38 25 28 grplid 
 |-  ( ( ( Scalar ` W ) e. Grp /\ ( z ( .i ` W ) z ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( +g ` ( Scalar ` W ) ) ( z ( .i ` W ) z ) ) = ( z ( .i ` W ) z ) )
42 37 40 41 syl2anc 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( +g ` ( Scalar ` W ) ) ( z ( .i ` W ) z ) ) = ( z ( .i ` W ) z ) )
43 27 34 42 3eqtrd 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( ( y ( +g ` W ) z ) ( .i ` W ) z ) = ( z ( .i ` W ) z ) )
44 simpr 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) )
45 2 24 23 28 3 ocvi 
 |-  ( ( ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) /\ z e. ( ._|_ ` S ) ) -> ( ( y ( +g ` W ) z ) ( .i ` W ) z ) = ( 0g ` ( Scalar ` W ) ) )
46 44 21 45 syl2anc 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( ( y ( +g ` W ) z ) ( .i ` W ) z ) = ( 0g ` ( Scalar ` W ) ) )
47 43 46 eqtr3d 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( z ( .i ` W ) z ) = ( 0g ` ( Scalar ` W ) ) )
48 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
49 23 24 2 28 48 ipeq0 
 |-  ( ( W e. PreHil /\ z e. V ) -> ( ( z ( .i ` W ) z ) = ( 0g ` ( Scalar ` W ) ) <-> z = ( 0g ` W ) ) )
50 17 22 49 syl2anc 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( ( z ( .i ` W ) z ) = ( 0g ` ( Scalar ` W ) ) <-> z = ( 0g ` W ) ) )
51 47 50 mpbid 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> z = ( 0g ` W ) )
52 51 oveq2d 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( y ( +g ` W ) z ) = ( y ( +g ` W ) ( 0g ` W ) ) )
53 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
54 10 53 syl 
 |-  ( ph -> W e. Grp )
55 54 ad2antrr 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> W e. Grp )
56 2 13 48 grprid 
 |-  ( ( W e. Grp /\ y e. V ) -> ( y ( +g ` W ) ( 0g ` W ) ) = y )
57 55 20 56 syl2anc 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( y ( +g ` W ) ( 0g ` W ) ) = y )
58 52 57 eqtrd 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( y ( +g ` W ) z ) = y )
59 58 19 eqeltrd 
 |-  ( ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) /\ ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) -> ( y ( +g ` W ) z ) e. S )
60 59 ex 
 |-  ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) -> ( ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) -> ( y ( +g ` W ) z ) e. S ) )
61 eleq1 
 |-  ( x = ( y ( +g ` W ) z ) -> ( x e. ( ._|_ ` ( ._|_ ` S ) ) <-> ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) ) )
62 eleq1 
 |-  ( x = ( y ( +g ` W ) z ) -> ( x e. S <-> ( y ( +g ` W ) z ) e. S ) )
63 61 62 imbi12d 
 |-  ( x = ( y ( +g ` W ) z ) -> ( ( x e. ( ._|_ ` ( ._|_ ` S ) ) -> x e. S ) <-> ( ( y ( +g ` W ) z ) e. ( ._|_ ` ( ._|_ ` S ) ) -> ( y ( +g ` W ) z ) e. S ) ) )
64 60 63 syl5ibrcom 
 |-  ( ( ph /\ ( y e. S /\ z e. ( ._|_ ` S ) ) ) -> ( x = ( y ( +g ` W ) z ) -> ( x e. ( ._|_ ` ( ._|_ ` S ) ) -> x e. S ) ) )
65 64 rexlimdvva 
 |-  ( ph -> ( E. y e. S E. z e. ( ._|_ ` S ) x = ( y ( +g ` W ) z ) -> ( x e. ( ._|_ ` ( ._|_ ` S ) ) -> x e. S ) ) )
66 16 65 syld 
 |-  ( ph -> ( x e. ( ._|_ ` ( ._|_ ` S ) ) -> ( x e. ( ._|_ ` ( ._|_ ` S ) ) -> x e. S ) ) )
67 66 pm2.43d 
 |-  ( ph -> ( x e. ( ._|_ ` ( ._|_ ` S ) ) -> x e. S ) )
68 67 ssrdv 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` S ) ) C_ S )
69 2 1 3 iscss2 
 |-  ( ( W e. PreHil /\ S C_ V ) -> ( S e. C <-> ( ._|_ ` ( ._|_ ` S ) ) C_ S ) )
70 5 6 69 syl2anc 
 |-  ( ph -> ( S e. C <-> ( ._|_ ` ( ._|_ ` S ) ) C_ S ) )
71 68 70 mpbird 
 |-  ( ph -> S e. C )