Metamath Proof Explorer

Theorem ipcnlem1

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

Ref Expression
Hypotheses ipcn.v 
|- V = ( Base ` W )
ipcn.h 
|- ., = ( .i ` W )
ipcn.d 
|- D = ( dist ` W )
ipcn.n 
|- N = ( norm ` W )
ipcn.t 
|- T = ( ( R / 2 ) / ( ( N ` A ) + 1 ) )
ipcn.u 
|- U = ( ( R / 2 ) / ( ( N ` B ) + T ) )
ipcn.w 
|- ( ph -> W e. CPreHil )
ipcn.a 
|- ( ph -> A e. V )
ipcn.b 
|- ( ph -> B e. V )
ipcn.r 
|- ( ph -> R e. RR+ )
Assertion ipcnlem1 
|- ( ph -> E. r e. RR+ A. x e. V A. y e. V ( ( ( A D x ) < r /\ ( B D y ) < r ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) )

Proof

Step Hyp Ref Expression
1 ipcn.v 
 |-  V = ( Base ` W )
2 ipcn.h 
 |-  ., = ( .i ` W )
3 ipcn.d 
 |-  D = ( dist ` W )
4 ipcn.n 
 |-  N = ( norm ` W )
5 ipcn.t 
 |-  T = ( ( R / 2 ) / ( ( N ` A ) + 1 ) )
6 ipcn.u 
 |-  U = ( ( R / 2 ) / ( ( N ` B ) + T ) )
7 ipcn.w 
 |-  ( ph -> W e. CPreHil )
8 ipcn.a 
 |-  ( ph -> A e. V )
9 ipcn.b 
 |-  ( ph -> B e. V )
10 ipcn.r 
 |-  ( ph -> R e. RR+ )
11 10 rphalfcld 
 |-  ( ph -> ( R / 2 ) e. RR+ )
12 cphnlm 
 |-  ( W e. CPreHil -> W e. NrmMod )
13 7 12 syl 
 |-  ( ph -> W e. NrmMod )
14 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
15 13 14 syl 
 |-  ( ph -> W e. NrmGrp )
16 1 4 nmcl 
 |-  ( ( W e. NrmGrp /\ A e. V ) -> ( N ` A ) e. RR )
17 15 8 16 syl2anc 
 |-  ( ph -> ( N ` A ) e. RR )
18 1 4 nmge0 
 |-  ( ( W e. NrmGrp /\ A e. V ) -> 0 <_ ( N ` A ) )
19 15 8 18 syl2anc 
 |-  ( ph -> 0 <_ ( N ` A ) )
20 17 19 ge0p1rpd 
 |-  ( ph -> ( ( N ` A ) + 1 ) e. RR+ )
21 11 20 rpdivcld 
 |-  ( ph -> ( ( R / 2 ) / ( ( N ` A ) + 1 ) ) e. RR+ )
22 5 21 eqeltrid 
 |-  ( ph -> T e. RR+ )
23 1 4 nmcl 
 |-  ( ( W e. NrmGrp /\ B e. V ) -> ( N ` B ) e. RR )
24 15 9 23 syl2anc 
 |-  ( ph -> ( N ` B ) e. RR )
25 22 rpred 
 |-  ( ph -> T e. RR )
26 24 25 readdcld 
 |-  ( ph -> ( ( N ` B ) + T ) e. RR )
27 0red 
 |-  ( ph -> 0 e. RR )
28 1 4 nmge0 
 |-  ( ( W e. NrmGrp /\ B e. V ) -> 0 <_ ( N ` B ) )
29 15 9 28 syl2anc 
 |-  ( ph -> 0 <_ ( N ` B ) )
30 24 22 ltaddrpd 
 |-  ( ph -> ( N ` B ) < ( ( N ` B ) + T ) )
31 27 24 26 29 30 lelttrd 
 |-  ( ph -> 0 < ( ( N ` B ) + T ) )
32 26 31 elrpd 
 |-  ( ph -> ( ( N ` B ) + T ) e. RR+ )
33 11 32 rpdivcld 
 |-  ( ph -> ( ( R / 2 ) / ( ( N ` B ) + T ) ) e. RR+ )
34 6 33 eqeltrid 
 |-  ( ph -> U e. RR+ )
35 22 34 ifcld 
 |-  ( ph -> if ( T <_ U , T , U ) e. RR+ )
36 7 adantr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> W e. CPreHil )
37 8 adantr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> A e. V )
38 9 adantr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> B e. V )
39 10 adantr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> R e. RR+ )
40 simprll 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> x e. V )
41 simprlr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> y e. V )
42 15 adantr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> W e. NrmGrp )
43 ngpms 
 |-  ( W e. NrmGrp -> W e. MetSp )
44 42 43 syl 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> W e. MetSp )
45 1 3 mscl 
 |-  ( ( W e. MetSp /\ A e. V /\ x e. V ) -> ( A D x ) e. RR )
46 44 37 40 45 syl3anc 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> ( A D x ) e. RR )
47 35 adantr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> if ( T <_ U , T , U ) e. RR+ )
48 47 rpred 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> if ( T <_ U , T , U ) e. RR )
49 34 rpred 
 |-  ( ph -> U e. RR )
50 49 adantr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> U e. RR )
51 simprrl 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> ( A D x ) < if ( T <_ U , T , U ) )
52 25 adantr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> T e. RR )
53 min2 
 |-  ( ( T e. RR /\ U e. RR ) -> if ( T <_ U , T , U ) <_ U )
54 52 50 53 syl2anc 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> if ( T <_ U , T , U ) <_ U )
55 46 48 50 51 54 ltletrd 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> ( A D x ) < U )
56 15 43 syl 
 |-  ( ph -> W e. MetSp )
57 56 adantr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> W e. MetSp )
58 1 3 mscl 
 |-  ( ( W e. MetSp /\ B e. V /\ y e. V ) -> ( B D y ) e. RR )
59 57 38 41 58 syl3anc 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> ( B D y ) e. RR )
60 simprrr 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> ( B D y ) < if ( T <_ U , T , U ) )
61 min1 
 |-  ( ( T e. RR /\ U e. RR ) -> if ( T <_ U , T , U ) <_ T )
62 52 50 61 syl2anc 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> if ( T <_ U , T , U ) <_ T )
63 59 48 52 60 62 ltletrd 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> ( B D y ) < T )
64 1 2 3 4 5 6 36 37 38 39 40 41 55 63 ipcnlem2 
 |-  ( ( ph /\ ( ( x e. V /\ y e. V ) /\ ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R )
65 64 expr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) )
66 65 ralrimivva 
 |-  ( ph -> A. x e. V A. y e. V ( ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) )
67 breq2 
 |-  ( r = if ( T <_ U , T , U ) -> ( ( A D x ) < r <-> ( A D x ) < if ( T <_ U , T , U ) ) )
68 breq2 
 |-  ( r = if ( T <_ U , T , U ) -> ( ( B D y ) < r <-> ( B D y ) < if ( T <_ U , T , U ) ) )
69 67 68 anbi12d 
 |-  ( r = if ( T <_ U , T , U ) -> ( ( ( A D x ) < r /\ ( B D y ) < r ) <-> ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) ) )
70 69 imbi1d 
 |-  ( r = if ( T <_ U , T , U ) -> ( ( ( ( A D x ) < r /\ ( B D y ) < r ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) <-> ( ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) ) )
71 70 2ralbidv 
 |-  ( r = if ( T <_ U , T , U ) -> ( A. x e. V A. y e. V ( ( ( A D x ) < r /\ ( B D y ) < r ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) <-> A. x e. V A. y e. V ( ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) ) )
72 71 rspcev 
 |-  ( ( if ( T <_ U , T , U ) e. RR+ /\ A. x e. V A. y e. V ( ( ( A D x ) < if ( T <_ U , T , U ) /\ ( B D y ) < if ( T <_ U , T , U ) ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) ) -> E. r e. RR+ A. x e. V A. y e. V ( ( ( A D x ) < r /\ ( B D y ) < r ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) )
73 35 66 72 syl2anc 
 |-  ( ph -> E. r e. RR+ A. x e. V A. y e. V ( ( ( A D x ) < r /\ ( B D y ) < r ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) )