Metamath Proof Explorer

Theorem clsocv

Description: The orthogonal complement of the closure of a subset is the same as the orthogonal complement of the subset itself. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses clsocv.v 
|- V = ( Base ` W )
clsocv.o 
|- O = ( ocv ` W )
clsocv.j 
|- J = ( TopOpen ` W )
Assertion clsocv 
|- ( ( W e. CPreHil /\ S C_ V ) -> ( O ` ( ( cls ` J ) ` S ) ) = ( O ` S ) )

Proof

Step Hyp Ref Expression
1 clsocv.v 
 |-  V = ( Base ` W )
2 clsocv.o 
 |-  O = ( ocv ` W )
3 clsocv.j 
 |-  J = ( TopOpen ` W )
4 cphngp 
 |-  ( W e. CPreHil -> W e. NrmGrp )
5 ngptps 
 |-  ( W e. NrmGrp -> W e. TopSp )
6 4 5 syl 
 |-  ( W e. CPreHil -> W e. TopSp )
7 6 adantr 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> W e. TopSp )
8 1 3 istps 
 |-  ( W e. TopSp <-> J e. ( TopOn ` V ) )
9 7 8 sylib 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> J e. ( TopOn ` V ) )
10 topontop 
 |-  ( J e. ( TopOn ` V ) -> J e. Top )
11 9 10 syl 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> J e. Top )
12 simpr 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> S C_ V )
13 toponuni 
 |-  ( J e. ( TopOn ` V ) -> V = U. J )
14 9 13 syl 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> V = U. J )
15 12 14 sseqtrd 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> S C_ U. J )
16 eqid 
 |-  U. J = U. J
17 16 sscls 
 |-  ( ( J e. Top /\ S C_ U. J ) -> S C_ ( ( cls ` J ) ` S ) )
18 11 15 17 syl2anc 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> S C_ ( ( cls ` J ) ` S ) )
19 2 ocv2ss 
 |-  ( S C_ ( ( cls ` J ) ` S ) -> ( O ` ( ( cls ` J ) ` S ) ) C_ ( O ` S ) )
20 18 19 syl 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> ( O ` ( ( cls ` J ) ` S ) ) C_ ( O ` S ) )
21 16 clsss3 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) C_ U. J )
22 11 15 21 syl2anc 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> ( ( cls ` J ) ` S ) C_ U. J )
23 22 14 sseqtrrd 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> ( ( cls ` J ) ` S ) C_ V )
24 23 adantr 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( ( cls ` J ) ` S ) C_ V )
25 1 2 ocvss 
 |-  ( O ` S ) C_ V
26 25 a1i 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> ( O ` S ) C_ V )
27 26 sselda 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> x e. V )
28 df-ss 
 |-  ( ( ( cls ` J ) ` S ) C_ V <-> ( ( ( cls ` J ) ` S ) i^i V ) = ( ( cls ` J ) ` S ) )
29 24 28 sylib 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( ( ( cls ` J ) ` S ) i^i V ) = ( ( cls ` J ) ` S ) )
30 29 ineq1d 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( ( ( ( cls ` J ) ` S ) i^i V ) i^i { y | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) = ( ( ( cls ` J ) ` S ) i^i { y | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) )
31 dfrab3 
 |-  { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } = ( V i^i { y | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
32 31 ineq2i 
 |-  ( ( ( cls ` J ) ` S ) i^i { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) = ( ( ( cls ` J ) ` S ) i^i ( V i^i { y | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) )
33 inass 
 |-  ( ( ( ( cls ` J ) ` S ) i^i V ) i^i { y | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) = ( ( ( cls ` J ) ` S ) i^i ( V i^i { y | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) )
34 32 33 eqtr4i 
 |-  ( ( ( cls ` J ) ` S ) i^i { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) = ( ( ( ( cls ` J ) ` S ) i^i V ) i^i { y | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
35 dfrab3 
 |-  { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } = ( ( ( cls ` J ) ` S ) i^i { y | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
36 30 34 35 3eqtr4g 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( ( ( cls ` J ) ` S ) i^i { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) = { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
37 16 clscld 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
38 11 15 37 syl2anc 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
39 38 adantr 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
40 fvex 
 |-  ( 0g ` ( Scalar ` W ) ) e. _V
41 eqid 
 |-  ( y e. V |-> ( x ( .i ` W ) y ) ) = ( y e. V |-> ( x ( .i ` W ) y ) )
42 41 mptiniseg 
 |-  ( ( 0g ` ( Scalar ` W ) ) e. _V -> ( `' ( y e. V |-> ( x ( .i ` W ) y ) ) " { ( 0g ` ( Scalar ` W ) ) } ) = { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
43 40 42 ax-mp 
 |-  ( `' ( y e. V |-> ( x ( .i ` W ) y ) ) " { ( 0g ` ( Scalar ` W ) ) } ) = { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) }
44 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
45 eqid 
 |-  ( .i ` W ) = ( .i ` W )
46 simpll 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> W e. CPreHil )
47 9 adantr 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> J e. ( TopOn ` V ) )
48 47 47 27 cnmptc 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( y e. V |-> x ) e. ( J Cn J ) )
49 47 cnmptid 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( y e. V |-> y ) e. ( J Cn J ) )
50 3 44 45 46 47 48 49 cnmpt1ip 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( y e. V |-> ( x ( .i ` W ) y ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
51 44 cnfldhaus 
 |-  ( TopOpen ` CCfld ) e. Haus
52 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
53 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
54 53 clm0 
 |-  ( W e. CMod -> 0 = ( 0g ` ( Scalar ` W ) ) )
55 52 54 syl 
 |-  ( W e. CPreHil -> 0 = ( 0g ` ( Scalar ` W ) ) )
56 55 ad2antrr 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> 0 = ( 0g ` ( Scalar ` W ) ) )
57 0cn 
 |-  0 e. CC
58 56 57 eqeltrrdi 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( 0g ` ( Scalar ` W ) ) e. CC )
59 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
60 59 sncld 
 |-  ( ( ( TopOpen ` CCfld ) e. Haus /\ ( 0g ` ( Scalar ` W ) ) e. CC ) -> { ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` ( TopOpen ` CCfld ) ) )
61 51 58 60 sylancr 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> { ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` ( TopOpen ` CCfld ) ) )
62 cnclima 
 |-  ( ( ( y e. V |-> ( x ( .i ` W ) y ) ) e. ( J Cn ( TopOpen ` CCfld ) ) /\ { ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` ( TopOpen ` CCfld ) ) ) -> ( `' ( y e. V |-> ( x ( .i ` W ) y ) ) " { ( 0g ` ( Scalar ` W ) ) } ) e. ( Clsd ` J ) )
63 50 61 62 syl2anc 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( `' ( y e. V |-> ( x ( .i ` W ) y ) ) " { ( 0g ` ( Scalar ` W ) ) } ) e. ( Clsd ` J ) )
64 43 63 eqeltrrid 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` J ) )
65 incld 
 |-  ( ( ( ( cls ` J ) ` S ) e. ( Clsd ` J ) /\ { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` J ) ) -> ( ( ( cls ` J ) ` S ) i^i { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) e. ( Clsd ` J ) )
66 39 64 65 syl2anc 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( ( ( cls ` J ) ` S ) i^i { y e. V | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) e. ( Clsd ` J ) )
67 36 66 eqeltrrd 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` J ) )
68 18 adantr 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> S C_ ( ( cls ` J ) ` S ) )
69 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
70 1 45 53 69 2 ocvi 
 |-  ( ( x e. ( O ` S ) /\ y e. S ) -> ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
71 70 ralrimiva 
 |-  ( x e. ( O ` S ) -> A. y e. S ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
72 71 adantl 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> A. y e. S ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
73 ssrab 
 |-  ( S C_ { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } <-> ( S C_ ( ( cls ` J ) ` S ) /\ A. y e. S ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
74 68 72 73 sylanbrc 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> S C_ { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
75 16 clsss2 
 |-  ( ( { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` J ) /\ S C_ { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) -> ( ( cls ` J ) ` S ) C_ { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
76 67 74 75 syl2anc 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( ( cls ` J ) ` S ) C_ { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
77 ssrab2 
 |-  { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } C_ ( ( cls ` J ) ` S )
78 77 a1i 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } C_ ( ( cls ` J ) ` S ) )
79 76 78 eqssd 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> ( ( cls ` J ) ` S ) = { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
80 rabid2 
 |-  ( ( ( cls ` J ) ` S ) = { y e. ( ( cls ` J ) ` S ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } <-> A. y e. ( ( cls ` J ) ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
81 79 80 sylib 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> A. y e. ( ( cls ` J ) ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
82 1 45 53 69 2 elocv 
 |-  ( x e. ( O ` ( ( cls ` J ) ` S ) ) <-> ( ( ( cls ` J ) ` S ) C_ V /\ x e. V /\ A. y e. ( ( cls ` J ) ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
83 24 27 81 82 syl3anbrc 
 |-  ( ( ( W e. CPreHil /\ S C_ V ) /\ x e. ( O ` S ) ) -> x e. ( O ` ( ( cls ` J ) ` S ) ) )
84 20 83 eqelssd 
 |-  ( ( W e. CPreHil /\ S C_ V ) -> ( O ` ( ( cls ` J ) ` S ) ) = ( O ` S ) )