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 β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) )