Metamath Proof Explorer

Theorem minveclem3

Description: Lemma for minvec . The filter formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses minvec.x ⊢ 𝑋 = ( Base ‘ 𝑈 )
minvec.m ⊢ − = ( -g ‘ 𝑈 )
minvec.n ⊢ 𝑁 = ( norm ‘ 𝑈 )
minvec.u ⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
minvec.y ⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
minvec.w ⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
minvec.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
minvec.j ⊢ 𝐽 = ( TopOpen ‘ 𝑈 )
minvec.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
minvec.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
minvec.d ⊢ 𝐷 = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
minvec.f ⊢ 𝐹 = ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } )
Assertion minveclem3 ( 𝜑 → ( 𝑌 filGen 𝐹 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 minvec.x ⊢ 𝑋 = ( Base ‘ 𝑈 )
2 minvec.m ⊢ − = ( -g ‘ 𝑈 )
3 minvec.n ⊢ 𝑁 = ( norm ‘ 𝑈 )
4 minvec.u ⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
5 minvec.y ⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
6 minvec.w ⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
7 minvec.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 minvec.j ⊢ 𝐽 = ( TopOpen ‘ 𝑈 )
9 minvec.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
10 minvec.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
11 minvec.d ⊢ 𝐷 = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
12 minvec.f ⊢ 𝐹 = ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → 𝑠 ∈ ℝ+ )
14 2z ⊢ 2 ∈ ℤ
15 rpexpcl ⊢ ( ( 𝑠 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑠 ↑ 2 ) ∈ ℝ+ )
16 13 14 15 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → ( 𝑠 ↑ 2 ) ∈ ℝ+ )
17 16 rphalfcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → ( ( 𝑠 ↑ 2 ) / 2 ) ∈ ℝ+ )
18 4nn ⊢ 4 ∈ ℕ
19 nnrp ⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
20 18 19 ax-mp ⊢ 4 ∈ ℝ+
21 rpdivcl ⊢ ( ( ( ( 𝑠 ↑ 2 ) / 2 ) ∈ ℝ+ ∧ 4 ∈ ℝ+ ) → ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ∈ ℝ+ )
22 17 20 21 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ∈ ℝ+ )
23 5 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
24 rabexg ⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∈ V )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∈ V )
26 eqid ⊢ ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) = ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } )
27 oveq2 ⊢ ( 𝑟 = ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) → ( ( 𝑆 ↑ 2 ) + 𝑟 ) = ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) )
28 27 breq2d ⊢ ( 𝑟 = ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) → ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) ↔ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) )
29 28 rabbidv ⊢ ( 𝑟 = ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } )
30 26 29 elrnmpt1s ⊢ ( ( ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ∈ ℝ+ ∧ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∈ V ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) )
31 22 25 30 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∈ ran ( 𝑟 ∈ ℝ+ ↦ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝑟 ) } ) )
32 31 12 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∈ 𝐹 )
33 oveq2 ⊢ ( 𝑦 = 𝑢 → ( 𝐴 𝐷 𝑦 ) = ( 𝐴 𝐷 𝑢 ) )
34 33 oveq1d ⊢ ( 𝑦 = 𝑢 → ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) = ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) )
35 34 breq1d ⊢ ( 𝑦 = 𝑢 → ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ↔ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) )
36 35 elrab ⊢ ( 𝑢 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ↔ ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) )
37 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐴 𝐷 𝑦 ) = ( 𝐴 𝐷 𝑣 ) )
38 37 oveq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) = ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) )
39 38 breq1d ⊢ ( 𝑦 = 𝑣 → ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ↔ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) )
40 39 elrab ⊢ ( 𝑣 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ↔ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) )
41 36 40 anbi12i ⊢ ( ( 𝑢 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∧ 𝑣 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ) ↔ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) )
42 simprll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝑢 ∈ 𝑌 )
43 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝑣 ∈ 𝑌 )
44 42 43 ovresd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) = ( 𝑢 𝐷 𝑣 ) )
45 cphngp ⊢ ( 𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp )
46 ngpms ⊢ ( 𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp )
47 1 11 msmet ⊢ ( 𝑈 ∈ MetSp → 𝐷 ∈ ( Met ‘ 𝑋 ) )
48 4 45 46 47 4syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
50 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
51 1 50 lssss ⊢ ( 𝑌 ∈ ( LSubSp ‘ 𝑈 ) → 𝑌 ⊆ 𝑋 )
52 5 51 syl ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝑌 ⊆ 𝑋 )
54 53 42 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝑢 ∈ 𝑋 )
55 53 43 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝑣 ∈ 𝑋 )
56 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) → ( 𝑢 𝐷 𝑣 ) ∈ ℝ )
57 49 54 55 56 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( 𝑢 𝐷 𝑣 ) ∈ ℝ )
58 57 resqcld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝑢 𝐷 𝑣 ) ↑ 2 ) ∈ ℝ )
59 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝑠 ↑ 2 ) / 2 ) ∈ ℝ+ )
60 59 rpred ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝑠 ↑ 2 ) / 2 ) ∈ ℝ )
61 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( 𝑠 ↑ 2 ) ∈ ℝ+ )
62 61 rpred ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( 𝑠 ↑ 2 ) ∈ ℝ )
63 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝑈 ∈ ℂPreHil )
64 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
65 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
66 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝐴 ∈ 𝑋 )
67 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ∈ ℝ+ )
68 67 rpred ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ∈ ℝ )
69 67 rpge0d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 0 ≤ ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) )
70 simprlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) )
71 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) )
72 1 2 3 63 64 65 66 8 9 10 11 68 69 42 43 70 71 minveclem2 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝑢 𝐷 𝑣 ) ↑ 2 ) ≤ ( 4 · ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) )
73 59 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝑠 ↑ 2 ) / 2 ) ∈ ℂ )
74 4cn ⊢ 4 ∈ ℂ
75 74 a1i ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 4 ∈ ℂ )
76 4ne0 ⊢ 4 ≠ 0
77 76 a1i ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 4 ≠ 0 )
78 73 75 77 divcan2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( 4 · ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) = ( ( 𝑠 ↑ 2 ) / 2 ) )
79 72 78 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝑢 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑠 ↑ 2 ) / 2 ) )
80 rphalflt ⊢ ( ( 𝑠 ↑ 2 ) ∈ ℝ+ → ( ( 𝑠 ↑ 2 ) / 2 ) < ( 𝑠 ↑ 2 ) )
81 61 80 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝑠 ↑ 2 ) / 2 ) < ( 𝑠 ↑ 2 ) )
82 58 60 62 79 81 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝑢 𝐷 𝑣 ) ↑ 2 ) < ( 𝑠 ↑ 2 ) )
83 rpre ⊢ ( 𝑠 ∈ ℝ+ → 𝑠 ∈ ℝ )
84 83 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 𝑠 ∈ ℝ )
85 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ) → 0 ≤ ( 𝑢 𝐷 𝑣 ) )
86 49 54 55 85 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 0 ≤ ( 𝑢 𝐷 𝑣 ) )
87 rpge0 ⊢ ( 𝑠 ∈ ℝ+ → 0 ≤ 𝑠 )
88 87 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → 0 ≤ 𝑠 )
89 57 84 86 88 lt2sqd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( ( 𝑢 𝐷 𝑣 ) < 𝑠 ↔ ( ( 𝑢 𝐷 𝑣 ) ↑ 2 ) < ( 𝑠 ↑ 2 ) ) )
90 82 89 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( 𝑢 𝐷 𝑣 ) < 𝑠 )
91 44 90 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( ( 𝑢 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑢 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ∧ ( 𝑣 ∈ 𝑌 ∧ ( ( 𝐴 𝐷 𝑣 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) ) ) ) → ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 )
92 41 91 sylan2b ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) ∧ ( 𝑢 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∧ 𝑣 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ) ) → ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 )
93 92 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → ∀ 𝑢 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∀ 𝑣 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 )
94 raleq ⊢ ( 𝑤 = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } → ( ∀ 𝑣 ∈ 𝑤 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 ↔ ∀ 𝑣 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 ) )
95 94 raleqbi1dv ⊢ ( 𝑤 = { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } → ( ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 ↔ ∀ 𝑢 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∀ 𝑣 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 ) )
96 95 rspcev ⊢ ( ( { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∈ 𝐹 ∧ ∀ 𝑢 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ∀ 𝑣 ∈ { 𝑦 ∈ 𝑌 ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( ( ( 𝑠 ↑ 2 ) / 2 ) / 4 ) ) } ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 ) → ∃ 𝑤 ∈ 𝐹 ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 )
97 32 93 96 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ+ ) → ∃ 𝑤 ∈ 𝐹 ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 )
98 97 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ ℝ+ ∃ 𝑤 ∈ 𝐹 ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 )
99 1 2 3 4 5 6 7 8 9 10 11 minveclem3a ⊢ ( 𝜑 → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) )
100 cmetmet ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) )
101 metxmet ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
102 99 100 101 3syl ⊢ ( 𝜑 → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
103 1 2 3 4 5 6 7 8 9 10 11 12 minveclem3b ⊢ ( 𝜑 → 𝐹 ∈ ( fBas ‘ 𝑌 ) )
104 fgcfil ⊢ ( ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( fBas ‘ 𝑌 ) ) → ( ( 𝑌 filGen 𝐹 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ↔ ∀ 𝑠 ∈ ℝ+ ∃ 𝑤 ∈ 𝐹 ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 ) )
105 102 103 104 syl2anc ⊢ ( 𝜑 → ( ( 𝑌 filGen 𝐹 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ↔ ∀ 𝑠 ∈ ℝ+ ∃ 𝑤 ∈ 𝐹 ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑠 ) )
106 98 105 mpbird ⊢ ( 𝜑 → ( 𝑌 filGen 𝐹 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )