This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
ipcn.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
ipcn.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
ipcn.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
ipcn.t ⊢ 𝑇 = ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐴 ) + 1 ) )
ipcn.u ⊢ 𝑈 = ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) )
ipcn.w ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
ipcn.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ipcn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
ipcn.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
ipcn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
ipcn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
ipcn.1 ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑋 ) < 𝑈 )
ipcn.2 ⊢ ( 𝜑 → ( 𝐵 𝐷 𝑌 ) < 𝑇 )
Assertion ipcnlem2 ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑋 , 𝑌 ) ) ) < 𝑅 )

Proof

Step Hyp Ref Expression
1 ipcn.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ipcn.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 ipcn.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
4 ipcn.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
5 ipcn.t ⊢ 𝑇 = ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐴 ) + 1 ) )
6 ipcn.u ⊢ 𝑈 = ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) )
7 ipcn.w ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
8 ipcn.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
9 ipcn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
10 ipcn.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
11 ipcn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12 ipcn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
13 ipcn.1 ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑋 ) < 𝑈 )
14 ipcn.2 ⊢ ( 𝜑 → ( 𝐵 𝐷 𝑌 ) < 𝑇 )
15 1 2 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ℂ )
16 7 8 9 15 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐵 ) ∈ ℂ )
17 1 2 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 , 𝑌 ) ∈ ℂ )
18 7 11 12 17 syl3anc ⊢ ( 𝜑 → ( 𝑋 , 𝑌 ) ∈ ℂ )
19 1 2 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐴 , 𝑌 ) ∈ ℂ )
20 7 8 12 19 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝑌 ) ∈ ℂ )
21 10 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
22 16 20 subcld ⊢ ( 𝜑 → ( ( 𝐴 , 𝐵 ) − ( 𝐴 , 𝑌 ) ) ∈ ℂ )
23 22 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝐴 , 𝑌 ) ) ) ∈ ℝ )
24 cphnlm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod )
25 7 24 syl ⊢ ( 𝜑 → 𝑊 ∈ NrmMod )
26 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
27 25 26 syl ⊢ ( 𝜑 → 𝑊 ∈ NrmGrp )
28 1 4 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
29 27 8 28 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
30 1 4 nmge0 ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
31 27 8 30 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
32 29 31 ge0p1rpd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) + 1 ) ∈ ℝ+ )
33 32 rpred ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) + 1 ) ∈ ℝ )
34 ngpms ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp )
35 27 34 syl ⊢ ( 𝜑 → 𝑊 ∈ MetSp )
36 1 3 mscl ⊢ ( ( 𝑊 ∈ MetSp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐵 𝐷 𝑌 ) ∈ ℝ )
37 35 9 12 36 syl3anc ⊢ ( 𝜑 → ( 𝐵 𝐷 𝑌 ) ∈ ℝ )
38 33 37 remulcld ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ 𝐴 ) + 1 ) · ( 𝐵 𝐷 𝑌 ) ) ∈ ℝ )
39 21 rehalfcld ⊢ ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ )
40 29 37 remulcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) · ( 𝐵 𝐷 𝑌 ) ) ∈ ℝ )
41 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
42 2 1 41 cphsubdi ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐴 , ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) = ( ( 𝐴 , 𝐵 ) − ( 𝐴 , 𝑌 ) ) )
43 7 8 9 12 42 syl13anc ⊢ ( 𝜑 → ( 𝐴 , ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) = ( ( 𝐴 , 𝐵 ) − ( 𝐴 , 𝑌 ) ) )
44 43 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 , ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) ) = ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝐴 , 𝑌 ) ) ) )
45 ngpgrp ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ Grp )
46 27 45 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
47 1 41 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
48 46 9 12 47 syl3anc ⊢ ( 𝜑 → ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
49 1 2 4 ipcau ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 ) → ( abs ‘ ( 𝐴 , ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) ) )
50 7 8 48 49 syl3anc ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 , ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) ) )
51 4 1 41 3 ngpds ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐵 𝐷 𝑌 ) = ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) )
52 27 9 12 51 syl3anc ⊢ ( 𝜑 → ( 𝐵 𝐷 𝑌 ) = ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) )
53 52 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) · ( 𝐵 𝐷 𝑌 ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) ) )
54 50 53 breqtrrd ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 , ( 𝐵 ( -g ‘ 𝑊 ) 𝑌 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝐵 𝐷 𝑌 ) ) )
55 44 54 eqbrtrrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝐴 , 𝑌 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) · ( 𝐵 𝐷 𝑌 ) ) )
56 msxms ⊢ ( 𝑊 ∈ MetSp → 𝑊 ∈ ∞MetSp )
57 35 56 syl ⊢ ( 𝜑 → 𝑊 ∈ ∞MetSp )
58 1 3 xmsge0 ⊢ ( ( 𝑊 ∈ ∞MetSp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 0 ≤ ( 𝐵 𝐷 𝑌 ) )
59 57 9 12 58 syl3anc ⊢ ( 𝜑 → 0 ≤ ( 𝐵 𝐷 𝑌 ) )
60 29 lep1d ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) ≤ ( ( 𝑁 ‘ 𝐴 ) + 1 ) )
61 29 33 37 59 60 lemul1ad ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) · ( 𝐵 𝐷 𝑌 ) ) ≤ ( ( ( 𝑁 ‘ 𝐴 ) + 1 ) · ( 𝐵 𝐷 𝑌 ) ) )
62 23 40 38 55 61 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝐴 , 𝑌 ) ) ) ≤ ( ( ( 𝑁 ‘ 𝐴 ) + 1 ) · ( 𝐵 𝐷 𝑌 ) ) )
63 14 5 breqtrdi ⊢ ( 𝜑 → ( 𝐵 𝐷 𝑌 ) < ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐴 ) + 1 ) ) )
64 37 39 32 ltmuldiv2d ⊢ ( 𝜑 → ( ( ( ( 𝑁 ‘ 𝐴 ) + 1 ) · ( 𝐵 𝐷 𝑌 ) ) < ( 𝑅 / 2 ) ↔ ( 𝐵 𝐷 𝑌 ) < ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐴 ) + 1 ) ) ) )
65 63 64 mpbird ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ 𝐴 ) + 1 ) · ( 𝐵 𝐷 𝑌 ) ) < ( 𝑅 / 2 ) )
66 23 38 39 62 65 lelttrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝐴 , 𝑌 ) ) ) < ( 𝑅 / 2 ) )
67 20 18 subcld ⊢ ( 𝜑 → ( ( 𝐴 , 𝑌 ) − ( 𝑋 , 𝑌 ) ) ∈ ℂ )
68 67 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝑌 ) − ( 𝑋 , 𝑌 ) ) ) ∈ ℝ )
69 1 3 mscl ⊢ ( ( 𝑊 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 𝐷 𝑋 ) ∈ ℝ )
70 35 8 11 69 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑋 ) ∈ ℝ )
71 1 4 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐵 ) ∈ ℝ )
72 27 9 71 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐵 ) ∈ ℝ )
73 10 rphalfcld ⊢ ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ+ )
74 73 32 rpdivcld ⊢ ( 𝜑 → ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐴 ) + 1 ) ) ∈ ℝ+ )
75 5 74 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
76 75 rpred ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
77 72 76 readdcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ∈ ℝ )
78 70 77 remulcld ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝑋 ) · ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) ∈ ℝ )
79 1 4 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑌 ) ∈ ℝ )
80 27 12 79 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑌 ) ∈ ℝ )
81 70 80 remulcld ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) ∈ ℝ )
82 2 1 41 cphsubdir ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) , 𝑌 ) = ( ( 𝐴 , 𝑌 ) − ( 𝑋 , 𝑌 ) ) )
83 7 8 11 12 82 syl13anc ⊢ ( 𝜑 → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) , 𝑌 ) = ( ( 𝐴 , 𝑌 ) − ( 𝑋 , 𝑌 ) ) )
84 83 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) , 𝑌 ) ) = ( abs ‘ ( ( 𝐴 , 𝑌 ) − ( 𝑋 , 𝑌 ) ) ) )
85 1 41 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) ∈ 𝑉 )
86 46 8 11 85 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) ∈ 𝑉 )
87 1 2 4 ipcau ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( abs ‘ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) , 𝑌 ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) ) · ( 𝑁 ‘ 𝑌 ) ) )
88 7 86 12 87 syl3anc ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) , 𝑌 ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) ) · ( 𝑁 ‘ 𝑌 ) ) )
89 4 1 41 3 ngpds ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 𝐷 𝑋 ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) ) )
90 27 8 11 89 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑋 ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) ) )
91 90 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) = ( ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) ) · ( 𝑁 ‘ 𝑌 ) ) )
92 88 91 breqtrrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝑋 ) , 𝑌 ) ) ≤ ( ( 𝐴 𝐷 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )
93 84 92 eqbrtrrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝑌 ) − ( 𝑋 , 𝑌 ) ) ) ≤ ( ( 𝐴 𝐷 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )
94 1 3 xmsge0 ⊢ ( ( 𝑊 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → 0 ≤ ( 𝐴 𝐷 𝑋 ) )
95 57 8 11 94 syl3anc ⊢ ( 𝜑 → 0 ≤ ( 𝐴 𝐷 𝑋 ) )
96 80 72 resubcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝐵 ) ) ∈ ℝ )
97 1 4 41 nm2dif ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ ( 𝑁 ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝐵 ) ) )
98 27 12 9 97 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ ( 𝑁 ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝐵 ) ) )
99 4 1 41 3 ngpdsr ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐵 𝐷 𝑌 ) = ( 𝑁 ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝐵 ) ) )
100 27 9 12 99 syl3anc ⊢ ( 𝜑 → ( 𝐵 𝐷 𝑌 ) = ( 𝑁 ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝐵 ) ) )
101 98 100 breqtrrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ ( 𝐵 𝐷 𝑌 ) )
102 37 76 14 ltled ⊢ ( 𝜑 → ( 𝐵 𝐷 𝑌 ) ≤ 𝑇 )
103 96 37 76 101 102 letrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ 𝑇 )
104 80 72 76 lesubadd2d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝐵 ) ) ≤ 𝑇 ↔ ( 𝑁 ‘ 𝑌 ) ≤ ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) )
105 103 104 mpbid ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑌 ) ≤ ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) )
106 80 77 70 95 105 lemul2ad ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) ≤ ( ( 𝐴 𝐷 𝑋 ) · ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) )
107 68 81 78 93 106 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝑌 ) − ( 𝑋 , 𝑌 ) ) ) ≤ ( ( 𝐴 𝐷 𝑋 ) · ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) )
108 13 6 breqtrdi ⊢ ( 𝜑 → ( 𝐴 𝐷 𝑋 ) < ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) )
109 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
110 1 4 nmge0 ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ) → 0 ≤ ( 𝑁 ‘ 𝐵 ) )
111 27 9 110 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ‘ 𝐵 ) )
112 72 75 ltaddrpd ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐵 ) < ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) )
113 109 72 77 111 112 lelttrd ⊢ ( 𝜑 → 0 < ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) )
114 ltmuldiv ⊢ ( ( ( 𝐴 𝐷 𝑋 ) ∈ ℝ ∧ ( 𝑅 / 2 ) ∈ ℝ ∧ ( ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ∈ ℝ ∧ 0 < ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) ) → ( ( ( 𝐴 𝐷 𝑋 ) · ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) < ( 𝑅 / 2 ) ↔ ( 𝐴 𝐷 𝑋 ) < ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) ) )
115 70 39 77 113 114 syl112anc ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝑋 ) · ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) < ( 𝑅 / 2 ) ↔ ( 𝐴 𝐷 𝑋 ) < ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) ) )
116 108 115 mpbird ⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝑋 ) · ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) < ( 𝑅 / 2 ) )
117 68 78 39 107 116 lelttrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝑌 ) − ( 𝑋 , 𝑌 ) ) ) < ( 𝑅 / 2 ) )
118 16 18 20 21 66 117 abs3lemd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑋 , 𝑌 ) ) ) < 𝑅 )