Metamath Proof Explorer

Theorem nlmvscnlem1

Description: Lemma for nlmvscn . (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses nlmvscn.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
nlmvscn.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
nlmvscn.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
nlmvscn.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
nlmvscn.e ⊢ 𝐸 = ( dist ‘ 𝐹 )
nlmvscn.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
nlmvscn.a ⊢ 𝐴 = ( norm ‘ 𝐹 )
nlmvscn.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
nlmvscn.t ⊢ 𝑇 = ( ( 𝑅 / 2 ) / ( ( 𝐴 ‘ 𝐵 ) + 1 ) )
nlmvscn.u ⊢ 𝑈 = ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) )
nlmvscn.w ⊢ ( 𝜑 → 𝑊 ∈ NrmMod )
nlmvscn.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
nlmvscn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
nlmvscn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion nlmvscnlem1 ( 𝜑 → ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )

Proof

Step Hyp Ref Expression
1 nlmvscn.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 nlmvscn.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 nlmvscn.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
4 nlmvscn.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
5 nlmvscn.e ⊢ 𝐸 = ( dist ‘ 𝐹 )
6 nlmvscn.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
7 nlmvscn.a ⊢ 𝐴 = ( norm ‘ 𝐹 )
8 nlmvscn.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
9 nlmvscn.t ⊢ 𝑇 = ( ( 𝑅 / 2 ) / ( ( 𝐴 ‘ 𝐵 ) + 1 ) )
10 nlmvscn.u ⊢ 𝑈 = ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) )
11 nlmvscn.w ⊢ ( 𝜑 → 𝑊 ∈ NrmMod )
12 nlmvscn.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
13 nlmvscn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
14 nlmvscn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
15 12 rphalfcld ⊢ ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ+ )
16 1 nlmngp2 ⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp )
17 11 16 syl ⊢ ( 𝜑 → 𝐹 ∈ NrmGrp )
18 3 7 nmcl ⊢ ( ( 𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 ‘ 𝐵 ) ∈ ℝ )
19 17 13 18 syl2anc ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐵 ) ∈ ℝ )
20 3 7 nmge0 ⊢ ( ( 𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾 ) → 0 ≤ ( 𝐴 ‘ 𝐵 ) )
21 17 13 20 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝐴 ‘ 𝐵 ) )
22 19 21 ge0p1rpd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐵 ) + 1 ) ∈ ℝ+ )
23 15 22 rpdivcld ⊢ ( 𝜑 → ( ( 𝑅 / 2 ) / ( ( 𝐴 ‘ 𝐵 ) + 1 ) ) ∈ ℝ+ )
24 9 23 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
25 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
26 11 25 syl ⊢ ( 𝜑 → 𝑊 ∈ NrmGrp )
27 2 6 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) ∈ ℝ )
28 26 14 27 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ ℝ )
29 24 rpred ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
30 28 29 readdcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ∈ ℝ )
31 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
32 2 6 nmge0 ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ) → 0 ≤ ( 𝑁 ‘ 𝑋 ) )
33 26 14 32 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ‘ 𝑋 ) )
34 28 24 ltaddrpd ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) < ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) )
35 31 28 30 33 34 lelttrd ⊢ ( 𝜑 → 0 < ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) )
36 30 35 elrpd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ∈ ℝ+ )
37 15 36 rpdivcld ⊢ ( 𝜑 → ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) ∈ ℝ+ )
38 10 37 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
39 24 38 ifcld ⊢ ( 𝜑 → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∈ ℝ+ )
40 11 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑊 ∈ NrmMod )
41 12 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑅 ∈ ℝ+ )
42 13 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝐵 ∈ 𝐾 )
43 14 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑋 ∈ 𝑉 )
44 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑥 ∈ 𝐾 )
45 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑦 ∈ 𝑉 )
46 17 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝐹 ∈ NrmGrp )
47 ngpms ⊢ ( 𝐹 ∈ NrmGrp → 𝐹 ∈ MetSp )
48 46 47 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝐹 ∈ MetSp )
49 3 5 mscl ⊢ ( ( 𝐹 ∈ MetSp ∧ 𝐵 ∈ 𝐾 ∧ 𝑥 ∈ 𝐾 ) → ( 𝐵 𝐸 𝑥 ) ∈ ℝ )
50 48 42 44 49 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐵 𝐸 𝑥 ) ∈ ℝ )
51 39 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∈ ℝ+ )
52 51 rpred ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∈ ℝ )
53 38 rpred ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑈 ∈ ℝ )
55 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) )
56 29 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑇 ∈ ℝ )
57 min2 ⊢ ( ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ≤ 𝑈 )
58 56 54 57 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ≤ 𝑈 )
59 50 52 54 55 58 ltletrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝐵 𝐸 𝑥 ) < 𝑈 )
60 ngpms ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp )
61 26 60 syl ⊢ ( 𝜑 → 𝑊 ∈ MetSp )
62 61 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → 𝑊 ∈ MetSp )
63 2 4 mscl ⊢ ( ( 𝑊 ∈ MetSp ∧ 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑋 𝐷 𝑦 ) ∈ ℝ )
64 62 43 45 63 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝑋 𝐷 𝑦 ) ∈ ℝ )
65 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) )
66 min1 ⊢ ( ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ≤ 𝑇 )
67 56 54 66 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ≤ 𝑇 )
68 64 52 56 65 67 ltletrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( 𝑋 𝐷 𝑦 ) < 𝑇 )
69 1 2 3 4 5 6 7 8 9 10 40 41 42 43 44 45 59 68 nlmvscnlem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ∧ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 )
70 69 expr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )
71 70 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )
72 breq2 ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ↔ ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) )
73 breq2 ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ( 𝑋 𝐷 𝑦 ) < 𝑟 ↔ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) )
74 72 73 anbi12d ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) ↔ ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) ) )
75 74 imbi1d ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ↔ ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ) )
76 75 2ralbidv ⊢ ( 𝑟 = if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) → ( ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ) )
77 76 rspcev ⊢ ( ( if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∈ ℝ+ ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ∧ ( 𝑋 𝐷 𝑦 ) < if ( 𝑇 ≤ 𝑈 , 𝑇 , 𝑈 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) ) → ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )
78 39 71 77 syl2anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ+ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( ( ( 𝐵 𝐸 𝑥 ) < 𝑟 ∧ ( 𝑋 𝐷 𝑦 ) < 𝑟 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝑥 · 𝑦 ) ) < 𝑅 ) )