Metamath Proof Explorer

Theorem ipcnlem2

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+ )
ipcn.x 
|- ( ph -> X e. V )
ipcn.y 
|- ( ph -> Y e. V )
ipcn.1 
|- ( ph -> ( A D X ) < U )
ipcn.2 
|- ( ph -> ( B D Y ) < T )
Assertion ipcnlem2 
|- ( ph -> ( 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 ipcn.x 
 |-  ( ph -> X e. V )
12 ipcn.y 
 |-  ( ph -> Y e. V )
13 ipcn.1 
 |-  ( ph -> ( A D X ) < U )
14 ipcn.2 
 |-  ( ph -> ( B D Y ) < T )
15 1 2 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. CC )
16 7 8 9 15 syl3anc 
 |-  ( ph -> ( A ., B ) e. CC )
17 1 2 cphipcl 
 |-  ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> ( X ., Y ) e. CC )
18 7 11 12 17 syl3anc 
 |-  ( ph -> ( X ., Y ) e. CC )
19 1 2 cphipcl 
 |-  ( ( W e. CPreHil /\ A e. V /\ Y e. V ) -> ( A ., Y ) e. CC )
20 7 8 12 19 syl3anc 
 |-  ( ph -> ( A ., Y ) e. CC )
21 10 rpred 
 |-  ( ph -> R e. RR )
22 16 20 subcld 
 |-  ( ph -> ( ( A ., B ) - ( A ., Y ) ) e. CC )
23 22 abscld 
 |-  ( ph -> ( abs ` ( ( A ., B ) - ( A ., Y ) ) ) e. RR )
24 cphnlm 
 |-  ( W e. CPreHil -> W e. NrmMod )
25 7 24 syl 
 |-  ( ph -> W e. NrmMod )
26 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
27 25 26 syl 
 |-  ( ph -> W e. NrmGrp )
28 1 4 nmcl 
 |-  ( ( W e. NrmGrp /\ A e. V ) -> ( N ` A ) e. RR )
29 27 8 28 syl2anc 
 |-  ( ph -> ( N ` A ) e. RR )
30 1 4 nmge0 
 |-  ( ( W e. NrmGrp /\ A e. V ) -> 0 <_ ( N ` A ) )
31 27 8 30 syl2anc 
 |-  ( ph -> 0 <_ ( N ` A ) )
32 29 31 ge0p1rpd 
 |-  ( ph -> ( ( N ` A ) + 1 ) e. RR+ )
33 32 rpred 
 |-  ( ph -> ( ( N ` A ) + 1 ) e. RR )
34 ngpms 
 |-  ( W e. NrmGrp -> W e. MetSp )
35 27 34 syl 
 |-  ( ph -> W e. MetSp )
36 1 3 mscl 
 |-  ( ( W e. MetSp /\ B e. V /\ Y e. V ) -> ( B D Y ) e. RR )
37 35 9 12 36 syl3anc 
 |-  ( ph -> ( B D Y ) e. RR )
38 33 37 remulcld 
 |-  ( ph -> ( ( ( N ` A ) + 1 ) x. ( B D Y ) ) e. RR )
39 21 rehalfcld 
 |-  ( ph -> ( R / 2 ) e. RR )
40 29 37 remulcld 
 |-  ( ph -> ( ( N ` A ) x. ( B D Y ) ) e. RR )
41 eqid 
 |-  ( -g ` W ) = ( -g ` W )
42 2 1 41 cphsubdi 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ Y e. V ) ) -> ( A ., ( B ( -g ` W ) Y ) ) = ( ( A ., B ) - ( A ., Y ) ) )
43 7 8 9 12 42 syl13anc 
 |-  ( ph -> ( A ., ( B ( -g ` W ) Y ) ) = ( ( A ., B ) - ( A ., Y ) ) )
44 43 fveq2d 
 |-  ( ph -> ( abs ` ( A ., ( B ( -g ` W ) Y ) ) ) = ( abs ` ( ( A ., B ) - ( A ., Y ) ) ) )
45 ngpgrp 
 |-  ( W e. NrmGrp -> W e. Grp )
46 27 45 syl 
 |-  ( ph -> W e. Grp )
47 1 41 grpsubcl 
 |-  ( ( W e. Grp /\ B e. V /\ Y e. V ) -> ( B ( -g ` W ) Y ) e. V )
48 46 9 12 47 syl3anc 
 |-  ( ph -> ( B ( -g ` W ) Y ) e. V )
49 1 2 4 ipcau 
 |-  ( ( W e. CPreHil /\ A e. V /\ ( B ( -g ` W ) Y ) e. V ) -> ( abs ` ( A ., ( B ( -g ` W ) Y ) ) ) <_ ( ( N ` A ) x. ( N ` ( B ( -g ` W ) Y ) ) ) )
50 7 8 48 49 syl3anc 
 |-  ( ph -> ( abs ` ( A ., ( B ( -g ` W ) Y ) ) ) <_ ( ( N ` A ) x. ( N ` ( B ( -g ` W ) Y ) ) ) )
51 4 1 41 3 ngpds 
 |-  ( ( W e. NrmGrp /\ B e. V /\ Y e. V ) -> ( B D Y ) = ( N ` ( B ( -g ` W ) Y ) ) )
52 27 9 12 51 syl3anc 
 |-  ( ph -> ( B D Y ) = ( N ` ( B ( -g ` W ) Y ) ) )
53 52 oveq2d 
 |-  ( ph -> ( ( N ` A ) x. ( B D Y ) ) = ( ( N ` A ) x. ( N ` ( B ( -g ` W ) Y ) ) ) )
54 50 53 breqtrrd 
 |-  ( ph -> ( abs ` ( A ., ( B ( -g ` W ) Y ) ) ) <_ ( ( N ` A ) x. ( B D Y ) ) )
55 44 54 eqbrtrrd 
 |-  ( ph -> ( abs ` ( ( A ., B ) - ( A ., Y ) ) ) <_ ( ( N ` A ) x. ( B D Y ) ) )
56 msxms 
 |-  ( W e. MetSp -> W e. *MetSp )
57 35 56 syl 
 |-  ( ph -> W e. *MetSp )
58 1 3 xmsge0 
 |-  ( ( W e. *MetSp /\ B e. V /\ Y e. V ) -> 0 <_ ( B D Y ) )
59 57 9 12 58 syl3anc 
 |-  ( ph -> 0 <_ ( B D Y ) )
60 29 lep1d 
 |-  ( ph -> ( N ` A ) <_ ( ( N ` A ) + 1 ) )
61 29 33 37 59 60 lemul1ad 
 |-  ( ph -> ( ( N ` A ) x. ( B D Y ) ) <_ ( ( ( N ` A ) + 1 ) x. ( B D Y ) ) )
62 23 40 38 55 61 letrd 
 |-  ( ph -> ( abs ` ( ( A ., B ) - ( A ., Y ) ) ) <_ ( ( ( N ` A ) + 1 ) x. ( B D Y ) ) )
63 14 5 breqtrdi 
 |-  ( ph -> ( B D Y ) < ( ( R / 2 ) / ( ( N ` A ) + 1 ) ) )
64 37 39 32 ltmuldiv2d 
 |-  ( ph -> ( ( ( ( N ` A ) + 1 ) x. ( B D Y ) ) < ( R / 2 ) <-> ( B D Y ) < ( ( R / 2 ) / ( ( N ` A ) + 1 ) ) ) )
65 63 64 mpbird 
 |-  ( ph -> ( ( ( N ` A ) + 1 ) x. ( B D Y ) ) < ( R / 2 ) )
66 23 38 39 62 65 lelttrd 
 |-  ( ph -> ( abs ` ( ( A ., B ) - ( A ., Y ) ) ) < ( R / 2 ) )
67 20 18 subcld 
 |-  ( ph -> ( ( A ., Y ) - ( X ., Y ) ) e. CC )
68 67 abscld 
 |-  ( ph -> ( abs ` ( ( A ., Y ) - ( X ., Y ) ) ) e. RR )
69 1 3 mscl 
 |-  ( ( W e. MetSp /\ A e. V /\ X e. V ) -> ( A D X ) e. RR )
70 35 8 11 69 syl3anc 
 |-  ( ph -> ( A D X ) e. RR )
71 1 4 nmcl 
 |-  ( ( W e. NrmGrp /\ B e. V ) -> ( N ` B ) e. RR )
72 27 9 71 syl2anc 
 |-  ( ph -> ( N ` B ) e. RR )
73 10 rphalfcld 
 |-  ( ph -> ( R / 2 ) e. RR+ )
74 73 32 rpdivcld 
 |-  ( ph -> ( ( R / 2 ) / ( ( N ` A ) + 1 ) ) e. RR+ )
75 5 74 eqeltrid 
 |-  ( ph -> T e. RR+ )
76 75 rpred 
 |-  ( ph -> T e. RR )
77 72 76 readdcld 
 |-  ( ph -> ( ( N ` B ) + T ) e. RR )
78 70 77 remulcld 
 |-  ( ph -> ( ( A D X ) x. ( ( N ` B ) + T ) ) e. RR )
79 1 4 nmcl 
 |-  ( ( W e. NrmGrp /\ Y e. V ) -> ( N ` Y ) e. RR )
80 27 12 79 syl2anc 
 |-  ( ph -> ( N ` Y ) e. RR )
81 70 80 remulcld 
 |-  ( ph -> ( ( A D X ) x. ( N ` Y ) ) e. RR )
82 2 1 41 cphsubdir 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ X e. V /\ Y e. V ) ) -> ( ( A ( -g ` W ) X ) ., Y ) = ( ( A ., Y ) - ( X ., Y ) ) )
83 7 8 11 12 82 syl13anc 
 |-  ( ph -> ( ( A ( -g ` W ) X ) ., Y ) = ( ( A ., Y ) - ( X ., Y ) ) )
84 83 fveq2d 
 |-  ( ph -> ( abs ` ( ( A ( -g ` W ) X ) ., Y ) ) = ( abs ` ( ( A ., Y ) - ( X ., Y ) ) ) )
85 1 41 grpsubcl 
 |-  ( ( W e. Grp /\ A e. V /\ X e. V ) -> ( A ( -g ` W ) X ) e. V )
86 46 8 11 85 syl3anc 
 |-  ( ph -> ( A ( -g ` W ) X ) e. V )
87 1 2 4 ipcau 
 |-  ( ( W e. CPreHil /\ ( A ( -g ` W ) X ) e. V /\ Y e. V ) -> ( abs ` ( ( A ( -g ` W ) X ) ., Y ) ) <_ ( ( N ` ( A ( -g ` W ) X ) ) x. ( N ` Y ) ) )
88 7 86 12 87 syl3anc 
 |-  ( ph -> ( abs ` ( ( A ( -g ` W ) X ) ., Y ) ) <_ ( ( N ` ( A ( -g ` W ) X ) ) x. ( N ` Y ) ) )
89 4 1 41 3 ngpds 
 |-  ( ( W e. NrmGrp /\ A e. V /\ X e. V ) -> ( A D X ) = ( N ` ( A ( -g ` W ) X ) ) )
90 27 8 11 89 syl3anc 
 |-  ( ph -> ( A D X ) = ( N ` ( A ( -g ` W ) X ) ) )
91 90 oveq1d 
 |-  ( ph -> ( ( A D X ) x. ( N ` Y ) ) = ( ( N ` ( A ( -g ` W ) X ) ) x. ( N ` Y ) ) )
92 88 91 breqtrrd 
 |-  ( ph -> ( abs ` ( ( A ( -g ` W ) X ) ., Y ) ) <_ ( ( A D X ) x. ( N ` Y ) ) )
93 84 92 eqbrtrrd 
 |-  ( ph -> ( abs ` ( ( A ., Y ) - ( X ., Y ) ) ) <_ ( ( A D X ) x. ( N ` Y ) ) )
94 1 3 xmsge0 
 |-  ( ( W e. *MetSp /\ A e. V /\ X e. V ) -> 0 <_ ( A D X ) )
95 57 8 11 94 syl3anc 
 |-  ( ph -> 0 <_ ( A D X ) )
96 80 72 resubcld 
 |-  ( ph -> ( ( N ` Y ) - ( N ` B ) ) e. RR )
97 1 4 41 nm2dif 
 |-  ( ( W e. NrmGrp /\ Y e. V /\ B e. V ) -> ( ( N ` Y ) - ( N ` B ) ) <_ ( N ` ( Y ( -g ` W ) B ) ) )
98 27 12 9 97 syl3anc 
 |-  ( ph -> ( ( N ` Y ) - ( N ` B ) ) <_ ( N ` ( Y ( -g ` W ) B ) ) )
99 4 1 41 3 ngpdsr 
 |-  ( ( W e. NrmGrp /\ B e. V /\ Y e. V ) -> ( B D Y ) = ( N ` ( Y ( -g ` W ) B ) ) )
100 27 9 12 99 syl3anc 
 |-  ( ph -> ( B D Y ) = ( N ` ( Y ( -g ` W ) B ) ) )
101 98 100 breqtrrd 
 |-  ( ph -> ( ( N ` Y ) - ( N ` B ) ) <_ ( B D Y ) )
102 37 76 14 ltled 
 |-  ( ph -> ( B D Y ) <_ T )
103 96 37 76 101 102 letrd 
 |-  ( ph -> ( ( N ` Y ) - ( N ` B ) ) <_ T )
104 80 72 76 lesubadd2d 
 |-  ( ph -> ( ( ( N ` Y ) - ( N ` B ) ) <_ T <-> ( N ` Y ) <_ ( ( N ` B ) + T ) ) )
105 103 104 mpbid 
 |-  ( ph -> ( N ` Y ) <_ ( ( N ` B ) + T ) )
106 80 77 70 95 105 lemul2ad 
 |-  ( ph -> ( ( A D X ) x. ( N ` Y ) ) <_ ( ( A D X ) x. ( ( N ` B ) + T ) ) )
107 68 81 78 93 106 letrd 
 |-  ( ph -> ( abs ` ( ( A ., Y ) - ( X ., Y ) ) ) <_ ( ( A D X ) x. ( ( N ` B ) + T ) ) )
108 13 6 breqtrdi 
 |-  ( ph -> ( A D X ) < ( ( R / 2 ) / ( ( N ` B ) + T ) ) )
109 0red 
 |-  ( ph -> 0 e. RR )
110 1 4 nmge0 
 |-  ( ( W e. NrmGrp /\ B e. V ) -> 0 <_ ( N ` B ) )
111 27 9 110 syl2anc 
 |-  ( ph -> 0 <_ ( N ` B ) )
112 72 75 ltaddrpd 
 |-  ( ph -> ( N ` B ) < ( ( N ` B ) + T ) )
113 109 72 77 111 112 lelttrd 
 |-  ( ph -> 0 < ( ( N ` B ) + T ) )
114 ltmuldiv 
 |-  ( ( ( A D X ) e. RR /\ ( R / 2 ) e. RR /\ ( ( ( N ` B ) + T ) e. RR /\ 0 < ( ( N ` B ) + T ) ) ) -> ( ( ( A D X ) x. ( ( N ` B ) + T ) ) < ( R / 2 ) <-> ( A D X ) < ( ( R / 2 ) / ( ( N ` B ) + T ) ) ) )
115 70 39 77 113 114 syl112anc 
 |-  ( ph -> ( ( ( A D X ) x. ( ( N ` B ) + T ) ) < ( R / 2 ) <-> ( A D X ) < ( ( R / 2 ) / ( ( N ` B ) + T ) ) ) )
116 108 115 mpbird 
 |-  ( ph -> ( ( A D X ) x. ( ( N ` B ) + T ) ) < ( R / 2 ) )
117 68 78 39 107 116 lelttrd 
 |-  ( ph -> ( abs ` ( ( A ., Y ) - ( X ., Y ) ) ) < ( R / 2 ) )
118 16 18 20 21 66 117 abs3lemd 
 |-  ( ph -> ( abs ` ( ( A ., B ) - ( X ., Y ) ) ) < R )