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 ⊢ 𝑉 = ( 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 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
Assertion ipcnlem1 ( 𝜑 → ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐴 𝐷 𝑥 ) < 𝑟 ∧ ( 𝐵 𝐷 𝑦 ) < 𝑟 ) → ( 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 10 rphalfcld ⊢ ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ+ )
12 cphnlm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod )
13 7 12 syl ⊢ ( 𝜑 → 𝑊 ∈ NrmMod )
14 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
15 13 14 syl ⊢ ( 𝜑 → 𝑊 ∈ NrmGrp )
16 1 4 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
17 15 8 16 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
18 1 4 nmge0 ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
19 15 8 18 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
20 17 19 ge0p1rpd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐴 ) + 1 ) ∈ ℝ+ )
21 11 20 rpdivcld ⊢ ( 𝜑 → ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐴 ) + 1 ) ) ∈ ℝ+ )
22 5 21 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
23 1 4 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ 𝐵 ) ∈ ℝ )
24 15 9 23 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐵 ) ∈ ℝ )
25 22 rpred ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
26 24 25 readdcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ∈ ℝ )
27 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
28 1 4 nmge0 ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ) → 0 ≤ ( 𝑁 ‘ 𝐵 ) )
29 15 9 28 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ‘ 𝐵 ) )
30 24 22 ltaddrpd ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐵 ) < ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) )
31 27 24 26 29 30 lelttrd ⊢ ( 𝜑 → 0 < ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) )
32 26 31 elrpd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ∈ ℝ+ )
33 11 32 rpdivcld ⊢ ( 𝜑 → ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝐵 ) + 𝑇 ) ) ∈ ℝ+ )
34 6 33 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
35 22 34 ifcld ⊢ ( 𝜑 → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∈ ℝ+ )
36 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑊 ∈ ℂPreHil )
37 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝐴 ∈ 𝑉 )
38 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝐵 ∈ 𝑉 )
39 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑅 ∈ ℝ+ )
40 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑥 ∈ 𝑉 )
41 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑦 ∈ 𝑉 )
42 15 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑊 ∈ NrmGrp )
43 ngpms ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp )
44 42 43 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑊 ∈ MetSp )
45 1 3 mscl ⊢ ( ( 𝑊 ∈ MetSp ∧ 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 𝐷 𝑥 ) ∈ ℝ )
46 44 37 40 45 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐴 𝐷 𝑥 ) ∈ ℝ )
47 35 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∈ ℝ+ )
48 47 rpred ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∈ ℝ )
49 34 rpred ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
50 49 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑈 ∈ ℝ )
51 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) )
52 25 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑇 ∈ ℝ )
53 min2 ⊢ ( ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ≤ 𝑈 )
54 52 50 53 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ≤ 𝑈 )
55 46 48 50 51 54 ltletrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐴 𝐷 𝑥 ) < 𝑈 )
56 15 43 syl ⊢ ( 𝜑 → 𝑊 ∈ MetSp )
57 56 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑊 ∈ MetSp )
58 1 3 mscl ⊢ ( ( 𝑊 ∈ MetSp ∧ 𝐵 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐵 𝐷 𝑦 ) ∈ ℝ )
59 57 38 41 58 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐵 𝐷 𝑦 ) ∈ ℝ )
60 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) )
61 min1 ⊢ ( ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ≤ 𝑇 )
62 52 50 61 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ≤ 𝑇 )
63 59 48 52 60 62 ltletrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐵 𝐷 𝑦 ) < 𝑇 )
64 1 2 3 4 5 6 36 37 38 39 40 41 55 63 ipcnlem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 )
65 64 expr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 ) )
66 65 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 ) )
67 breq2 ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ( 𝐴 𝐷 𝑥 ) < 𝑟 ↔ ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) )
68 breq2 ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ( 𝐵 𝐷 𝑦 ) < 𝑟 ↔ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) )
69 67 68 anbi12d ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ( ( 𝐴 𝐷 𝑥 ) < 𝑟 ∧ ( 𝐵 𝐷 𝑦 ) < 𝑟 ) ↔ ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) )
70 69 imbi1d ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ( ( ( 𝐴 𝐷 𝑥 ) < 𝑟 ∧ ( 𝐵 𝐷 𝑦 ) < 𝑟 ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 ) ↔ ( ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 ) ) )
71 70 2ralbidv ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐴 𝐷 𝑥 ) < 𝑟 ∧ ( 𝐵 𝐷 𝑦 ) < 𝑟 ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 ) ) )
72 71 rspcev ⊢ ( ( if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∈ ℝ+ ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐴 𝐷 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝐵 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 ) ) → ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐴 𝐷 𝑥 ) < 𝑟 ∧ ( 𝐵 𝐷 𝑦 ) < 𝑟 ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 ) )
73 35 66 72 syl2anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐴 𝐷 𝑥 ) < 𝑟 ∧ ( 𝐵 𝐷 𝑦 ) < 𝑟 ) → ( abs ‘ ( ( 𝐴 , 𝐵 ) − ( 𝑥 , 𝑦 ) ) ) < 𝑅 ) )