Metamath Proof Explorer

Theorem csscld

Description: A "closed subspace" in a subcomplex pre-Hilbert space is actually closed in the topology induced by the norm, thus justifying the terminology "closed subspace". (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses csscld.c 
|- C = ( ClSubSp ` W )
csscld.j 
|- J = ( TopOpen ` W )
Assertion csscld 
|- ( ( W e. CPreHil /\ S e. C ) -> S e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 csscld.c 
 |-  C = ( ClSubSp ` W )
2 csscld.j 
 |-  J = ( TopOpen ` W )
3 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
4 3 1 cssi 
 |-  ( S e. C -> S = ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) )
5 4 adantl 
 |-  ( ( W e. CPreHil /\ S e. C ) -> S = ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 6 3 ocvss 
 |-  ( ( ocv ` W ) ` S ) C_ ( Base ` W )
8 eqid 
 |-  ( .i ` W ) = ( .i ` W )
9 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
10 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
11 6 8 9 10 3 ocvval 
 |-  ( ( ( ocv ` W ) ` S ) C_ ( Base ` W ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) = { x e. ( Base ` W ) | A. y e. ( ( ocv ` W ) ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
12 7 11 mp1i 
 |-  ( ( W e. CPreHil /\ S e. C ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) = { x e. ( Base ` W ) | A. y e. ( ( ocv ` W ) ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
13 riinrab 
 |-  ( ( Base ` W ) i^i |^|_ y e. ( ( ocv ` W ) ` S ) { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) = { x e. ( Base ` W ) | A. y e. ( ( ocv ` W ) ` S ) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) }
14 12 13 eqtr4di 
 |-  ( ( W e. CPreHil /\ S e. C ) -> ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) = ( ( Base ` W ) i^i |^|_ y e. ( ( ocv ` W ) ` S ) { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) )
15 cphnlm 
 |-  ( W e. CPreHil -> W e. NrmMod )
16 15 adantr 
 |-  ( ( W e. CPreHil /\ S e. C ) -> W e. NrmMod )
17 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
18 ngptps 
 |-  ( W e. NrmGrp -> W e. TopSp )
19 16 17 18 3syl 
 |-  ( ( W e. CPreHil /\ S e. C ) -> W e. TopSp )
20 6 2 istps 
 |-  ( W e. TopSp <-> J e. ( TopOn ` ( Base ` W ) ) )
21 19 20 sylib 
 |-  ( ( W e. CPreHil /\ S e. C ) -> J e. ( TopOn ` ( Base ` W ) ) )
22 toponuni 
 |-  ( J e. ( TopOn ` ( Base ` W ) ) -> ( Base ` W ) = U. J )
23 21 22 syl 
 |-  ( ( W e. CPreHil /\ S e. C ) -> ( Base ` W ) = U. J )
24 23 ineq1d 
 |-  ( ( W e. CPreHil /\ S e. C ) -> ( ( Base ` W ) i^i |^|_ y e. ( ( ocv ` W ) ` S ) { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) = ( U. J i^i |^|_ y e. ( ( ocv ` W ) ` S ) { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) )
25 5 14 24 3eqtrd 
 |-  ( ( W e. CPreHil /\ S e. C ) -> S = ( U. J i^i |^|_ y e. ( ( ocv ` W ) ` S ) { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) )
26 topontop 
 |-  ( J e. ( TopOn ` ( Base ` W ) ) -> J e. Top )
27 21 26 syl 
 |-  ( ( W e. CPreHil /\ S e. C ) -> J e. Top )
28 7 sseli 
 |-  ( y e. ( ( ocv ` W ) ` S ) -> y e. ( Base ` W ) )
29 fvex 
 |-  ( 0g ` ( Scalar ` W ) ) e. _V
30 eqid 
 |-  ( x e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) = ( x e. ( Base ` W ) |-> ( x ( .i ` W ) y ) )
31 30 mptiniseg 
 |-  ( ( 0g ` ( Scalar ` W ) ) e. _V -> ( `' ( x e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) " { ( 0g ` ( Scalar ` W ) ) } ) = { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
32 29 31 ax-mp 
 |-  ( `' ( x e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) " { ( 0g ` ( Scalar ` W ) ) } ) = { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) }
33 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
34 simpll 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> W e. CPreHil )
35 21 adantr 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> J e. ( TopOn ` ( Base ` W ) ) )
36 35 cnmptid 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> ( x e. ( Base ` W ) |-> x ) e. ( J Cn J ) )
37 simpr 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> y e. ( Base ` W ) )
38 35 35 37 cnmptc 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> ( x e. ( Base ` W ) |-> y ) e. ( J Cn J ) )
39 2 33 8 34 35 36 38 cnmpt1ip 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> ( x e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) e. ( J Cn ( TopOpen ` CCfld ) ) )
40 33 cnfldhaus 
 |-  ( TopOpen ` CCfld ) e. Haus
41 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
42 9 clm0 
 |-  ( W e. CMod -> 0 = ( 0g ` ( Scalar ` W ) ) )
43 41 42 syl 
 |-  ( W e. CPreHil -> 0 = ( 0g ` ( Scalar ` W ) ) )
44 43 ad2antrr 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> 0 = ( 0g ` ( Scalar ` W ) ) )
45 0cn 
 |-  0 e. CC
46 44 45 eqeltrrdi 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> ( 0g ` ( Scalar ` W ) ) e. CC )
47 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
48 47 sncld 
 |-  ( ( ( TopOpen ` CCfld ) e. Haus /\ ( 0g ` ( Scalar ` W ) ) e. CC ) -> { ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` ( TopOpen ` CCfld ) ) )
49 40 46 48 sylancr 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> { ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` ( TopOpen ` CCfld ) ) )
50 cnclima 
 |-  ( ( ( x e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) e. ( J Cn ( TopOpen ` CCfld ) ) /\ { ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` ( TopOpen ` CCfld ) ) ) -> ( `' ( x e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) " { ( 0g ` ( Scalar ` W ) ) } ) e. ( Clsd ` J ) )
51 39 49 50 syl2anc 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> ( `' ( x e. ( Base ` W ) |-> ( x ( .i ` W ) y ) ) " { ( 0g ` ( Scalar ` W ) ) } ) e. ( Clsd ` J ) )
52 32 51 eqeltrrid 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( Base ` W ) ) -> { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` J ) )
53 28 52 sylan2 
 |-  ( ( ( W e. CPreHil /\ S e. C ) /\ y e. ( ( ocv ` W ) ` S ) ) -> { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` J ) )
54 53 ralrimiva 
 |-  ( ( W e. CPreHil /\ S e. C ) -> A. y e. ( ( ocv ` W ) ` S ) { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` J ) )
55 eqid 
 |-  U. J = U. J
56 55 riincld 
 |-  ( ( J e. Top /\ A. y e. ( ( ocv ` W ) ` S ) { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } e. ( Clsd ` J ) ) -> ( U. J i^i |^|_ y e. ( ( ocv ` W ) ` S ) { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) e. ( Clsd ` J ) )
57 27 54 56 syl2anc 
 |-  ( ( W e. CPreHil /\ S e. C ) -> ( U. J i^i |^|_ y e. ( ( ocv ` W ) ` S ) { x e. ( Base ` W ) | ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } ) e. ( Clsd ` J ) )
58 25 57 eqeltrd 
 |-  ( ( W e. CPreHil /\ S e. C ) -> S e. ( Clsd ` J ) )