Metamath Proof Explorer

Theorem ipcn

Description: The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ipcn.f 
|- ., = ( .if ` W )
ipcn.j 
|- J = ( TopOpen ` W )
ipcn.k 
|- K = ( TopOpen ` CCfld )
Assertion ipcn 
|- ( W e. CPreHil -> ., e. ( ( J tX J ) Cn K ) )

Proof

Step Hyp Ref Expression
1 ipcn.f 
 |-  ., = ( .if ` W )
2 ipcn.j 
 |-  J = ( TopOpen ` W )
3 ipcn.k 
 |-  K = ( TopOpen ` CCfld )
4 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
5 eqid 
 |-  ( Base ` W ) = ( Base ` W )
6 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
7 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
8 5 1 6 7 phlipf 
 |-  ( W e. PreHil -> ., : ( ( Base ` W ) X. ( Base ` W ) ) --> ( Base ` ( Scalar ` W ) ) )
9 4 8 syl 
 |-  ( W e. CPreHil -> ., : ( ( Base ` W ) X. ( Base ` W ) ) --> ( Base ` ( Scalar ` W ) ) )
10 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
11 6 7 clmsscn 
 |-  ( W e. CMod -> ( Base ` ( Scalar ` W ) ) C_ CC )
12 10 11 syl 
 |-  ( W e. CPreHil -> ( Base ` ( Scalar ` W ) ) C_ CC )
13 9 12 fssd 
 |-  ( W e. CPreHil -> ., : ( ( Base ` W ) X. ( Base ` W ) ) --> CC )
14 eqid 
 |-  ( .i ` W ) = ( .i ` W )
15 eqid 
 |-  ( dist ` W ) = ( dist ` W )
16 eqid 
 |-  ( norm ` W ) = ( norm ` W )
17 eqid 
 |-  ( ( r / 2 ) / ( ( ( norm ` W ) ` x ) + 1 ) ) = ( ( r / 2 ) / ( ( ( norm ` W ) ` x ) + 1 ) )
18 eqid 
 |-  ( ( r / 2 ) / ( ( ( norm ` W ) ` y ) + ( ( r / 2 ) / ( ( ( norm ` W ) ` x ) + 1 ) ) ) ) = ( ( r / 2 ) / ( ( ( norm ` W ) ` y ) + ( ( r / 2 ) / ( ( ( norm ` W ) ` x ) + 1 ) ) ) )
19 simpll 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> W e. CPreHil )
20 simplrl 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> x e. ( Base ` W ) )
21 simplrr 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> y e. ( Base ` W ) )
22 simpr 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> r e. RR+ )
23 5 14 15 16 17 18 19 20 21 22 ipcnlem1 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ r e. RR+ ) -> E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( dist ` W ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( abs ` ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) ) < r ) )
24 23 ralrimiva 
 |-  ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> A. r e. RR+ E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( dist ` W ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( abs ` ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) ) < r ) )
25 simplrl 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> x e. ( Base ` W ) )
26 simprl 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> z e. ( Base ` W ) )
27 25 26 ovresd 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) = ( x ( dist ` W ) z ) )
28 27 breq1d 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s <-> ( x ( dist ` W ) z ) < s ) )
29 simplrr 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
30 simprr 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> w e. ( Base ` W ) )
31 29 30 ovresd 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) = ( y ( dist ` W ) w ) )
32 31 breq1d 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s <-> ( y ( dist ` W ) w ) < s ) )
33 28 32 anbi12d 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) <-> ( ( x ( dist ` W ) z ) < s /\ ( y ( dist ` W ) w ) < s ) ) )
34 13 ad2antrr 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ., : ( ( Base ` W ) X. ( Base ` W ) ) --> CC )
35 34 25 29 fovrnd 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( x ., y ) e. CC )
36 34 26 30 fovrnd 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( z ., w ) e. CC )
37 eqid 
 |-  ( abs o. - ) = ( abs o. - )
38 37 cnmetdval 
 |-  ( ( ( x ., y ) e. CC /\ ( z ., w ) e. CC ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) = ( abs ` ( ( x ., y ) - ( z ., w ) ) ) )
39 35 36 38 syl2anc 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) = ( abs ` ( ( x ., y ) - ( z ., w ) ) ) )
40 5 14 1 ipfval 
 |-  ( ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( x ., y ) = ( x ( .i ` W ) y ) )
41 25 29 40 syl2anc 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( x ., y ) = ( x ( .i ` W ) y ) )
42 5 14 1 ipfval 
 |-  ( ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) -> ( z ., w ) = ( z ( .i ` W ) w ) )
43 42 adantl 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( z ., w ) = ( z ( .i ` W ) w ) )
44 41 43 oveq12d 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( ( x ., y ) - ( z ., w ) ) = ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) )
45 44 fveq2d 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( abs ` ( ( x ., y ) - ( z ., w ) ) ) = ( abs ` ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) ) )
46 39 45 eqtrd 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) = ( abs ` ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) ) )
47 46 breq1d 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( ( ( x ., y ) ( abs o. - ) ( z ., w ) ) < r <-> ( abs ` ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) ) < r ) )
48 33 47 imbi12d 
 |-  ( ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) /\ ( z e. ( Base ` W ) /\ w e. ( Base ` W ) ) ) -> ( ( ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) < r ) <-> ( ( ( x ( dist ` W ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( abs ` ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) ) < r ) ) )
49 48 2ralbidva 
 |-  ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) < r ) <-> A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( dist ` W ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( abs ` ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) ) < r ) ) )
50 49 rexbidv 
 |-  ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) < r ) <-> E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( dist ` W ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( abs ` ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) ) < r ) ) )
51 50 ralbidv 
 |-  ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( A. r e. RR+ E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) < r ) <-> A. r e. RR+ E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( dist ` W ) z ) < s /\ ( y ( dist ` W ) w ) < s ) -> ( abs ` ( ( x ( .i ` W ) y ) - ( z ( .i ` W ) w ) ) ) < r ) ) )
52 24 51 mpbird 
 |-  ( ( W e. CPreHil /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> A. r e. RR+ E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) < r ) )
53 52 ralrimivva 
 |-  ( W e. CPreHil -> A. x e. ( Base ` W ) A. y e. ( Base ` W ) A. r e. RR+ E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) < r ) )
54 cphngp 
 |-  ( W e. CPreHil -> W e. NrmGrp )
55 ngpms 
 |-  ( W e. NrmGrp -> W e. MetSp )
56 54 55 syl 
 |-  ( W e. CPreHil -> W e. MetSp )
57 msxms 
 |-  ( W e. MetSp -> W e. *MetSp )
58 56 57 syl 
 |-  ( W e. CPreHil -> W e. *MetSp )
59 eqid 
 |-  ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) = ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) )
60 5 59 xmsxmet 
 |-  ( W e. *MetSp -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) )
61 58 60 syl 
 |-  ( W e. CPreHil -> ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) )
62 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
63 62 a1i 
 |-  ( W e. CPreHil -> ( abs o. - ) e. ( *Met ` CC ) )
64 eqid 
 |-  ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) )
65 3 cnfldtopn 
 |-  K = ( MetOpen ` ( abs o. - ) )
66 64 64 65 txmetcn 
 |-  ( ( ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) /\ ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) e. ( *Met ` ( Base ` W ) ) /\ ( abs o. - ) e. ( *Met ` CC ) ) -> ( ., e. ( ( ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) Cn K ) <-> ( ., : ( ( Base ` W ) X. ( Base ` W ) ) --> CC /\ A. x e. ( Base ` W ) A. y e. ( Base ` W ) A. r e. RR+ E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) < r ) ) ) )
67 61 61 63 66 syl3anc 
 |-  ( W e. CPreHil -> ( ., e. ( ( ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) Cn K ) <-> ( ., : ( ( Base ` W ) X. ( Base ` W ) ) --> CC /\ A. x e. ( Base ` W ) A. y e. ( Base ` W ) A. r e. RR+ E. s e. RR+ A. z e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( x ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) z ) < s /\ ( y ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) w ) < s ) -> ( ( x ., y ) ( abs o. - ) ( z ., w ) ) < r ) ) ) )
68 13 53 67 mpbir2and 
 |-  ( W e. CPreHil -> ., e. ( ( ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) Cn K ) )
69 2 5 59 mstopn 
 |-  ( W e. MetSp -> J = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) )
70 56 69 syl 
 |-  ( W e. CPreHil -> J = ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) )
71 70 70 oveq12d 
 |-  ( W e. CPreHil -> ( J tX J ) = ( ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) )
72 71 oveq1d 
 |-  ( W e. CPreHil -> ( ( J tX J ) Cn K ) = ( ( ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) tX ( MetOpen ` ( ( dist ` W ) |` ( ( Base ` W ) X. ( Base ` W ) ) ) ) ) Cn K ) )
73 68 72 eleqtrrd 
 |-  ( W e. CPreHil -> ., e. ( ( J tX J ) Cn K ) )