Metamath Proof Explorer

Theorem minvecolem5

Description: Lemma for minveco . Discharge the assumption about the sequence F by applying countable choice ax-cc . (Contributed by Mario Carneiro, 9-May-2014) (Revised by AV, 4-Oct-2020) (New usage is discouraged.)

Ref Expression
Hypotheses minveco.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
minveco.m ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
minveco.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
minveco.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
minveco.u ⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
minveco.w ⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
minveco.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
minveco.d ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
minveco.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
minveco.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
minveco.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
Assertion minvecolem5 ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 minveco.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 minveco.m ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3 minveco.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 minveco.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5 minveco.u ⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
6 minveco.w ⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
7 minveco.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 minveco.d ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
9 minveco.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
10 minveco.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
11 minveco.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
12 nnrecgt0 ⊢ ( 𝑛 ∈ ℕ → 0 < ( 1 / 𝑛 ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 < ( 1 / 𝑛 ) )
14 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
16 1 2 3 4 5 6 7 8 9 10 minvecolem1 ⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
18 17 simp1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑅 ⊆ ℝ )
19 17 simp2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑅 ≠ ∅ )
20 0re ⊢ 0 ∈ ℝ
21 17 simp3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
22 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
23 22 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
24 23 rspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
25 20 21 24 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
26 infrecl ⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
27 18 19 25 26 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
28 11 27 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑆 ∈ ℝ )
29 28 resqcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ↑ 2 ) ∈ ℝ )
30 15 29 ltaddposd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 0 < ( 1 / 𝑛 ) ↔ ( 𝑆 ↑ 2 ) < ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
31 13 30 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ↑ 2 ) < ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
32 29 15 readdcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ∈ ℝ )
33 28 sqge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( 𝑆 ↑ 2 ) )
34 29 15 33 13 addgegt0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 < ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
35 32 34 elrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ∈ ℝ+ )
36 35 rpge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
37 resqrtth ⊢ ( ( ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ↑ 2 ) = ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
38 32 36 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ↑ 2 ) = ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
39 31 38 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 ↑ 2 ) < ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ↑ 2 ) )
40 35 rpsqrtcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ∈ ℝ+ )
41 40 rpred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ∈ ℝ )
42 0red ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ∈ ℝ )
43 infregelb ⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ 0 ∈ ℝ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
44 18 19 25 42 43 syl31anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
45 21 44 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ inf ( 𝑅 , ℝ , < ) )
46 45 11 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ 𝑆 )
47 32 36 sqrtge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
48 28 41 46 47 lt2sqd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 < ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ↔ ( 𝑆 ↑ 2 ) < ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ↑ 2 ) ) )
49 39 48 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑆 < ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
50 28 41 ltnled ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑆 < ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ↔ ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑆 ) )
51 49 50 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑆 )
52 11 breq2i ⊢ ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑆 ↔ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ inf ( 𝑅 , ℝ , < ) )
53 infregelb ⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ∈ ℝ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑤 ) )
54 18 19 25 41 53 syl31anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑤 ) )
55 52 54 syl5bb ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑆 ↔ ∀ 𝑤 ∈ 𝑅 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑤 ) )
56 10 raleqi ⊢ ( ∀ 𝑤 ∈ 𝑅 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑤 ↔ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑤 )
57 fvex ⊢ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
58 57 rgenw ⊢ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
59 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
60 breq2 ⊢ ( 𝑤 = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑤 ↔ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
61 59 60 ralrnmptw ⊢ ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V → ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
62 58 61 ax-mp ⊢ ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
63 56 62 bitri ⊢ ( ∀ 𝑤 ∈ 𝑅 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑤 ↔ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
64 55 63 bitrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ 𝑆 ↔ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
65 51 64 mtbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ¬ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
66 rexnal ⊢ ( ∃ 𝑦 ∈ 𝑌 ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↔ ¬ ∀ 𝑦 ∈ 𝑌 ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
67 65 66 sylibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑦 ∈ 𝑌 ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
68 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ∈ ℝ )
69 phnv ⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
70 5 69 syl ⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
71 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → 𝑈 ∈ NrmCVec )
72 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
73 inss1 ⊢ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ⊆ ( SubSp ‘ 𝑈 )
74 73 6 sselid ⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
75 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
76 1 4 75 sspba ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
77 70 74 76 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑌 ⊆ 𝑋 )
79 78 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 )
80 1 2 nvmcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 )
81 71 72 79 80 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 )
82 1 3 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ ℝ )
83 71 81 82 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ ℝ )
84 83 resqcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ∈ ℝ )
85 68 84 letrid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ∨ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
86 85 ord ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ¬ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
87 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ∈ ℝ )
88 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → 0 ≤ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
89 1 3 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
90 71 81 89 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → 0 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
91 87 83 88 90 le2sqd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↔ ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ) )
92 38 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ↑ 2 ) = ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
93 92 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ↔ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ) )
94 91 93 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↔ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ) )
95 94 notbid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↔ ¬ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ) )
96 1 2 3 8 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
97 71 72 79 96 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
98 97 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) )
99 98 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ↔ ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
100 86 95 99 3imtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑌 ) → ( ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) → ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
101 100 reximdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∃ 𝑦 ∈ 𝑌 ¬ ( √ ‘ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) → ∃ 𝑦 ∈ 𝑌 ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
102 67 101 mpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑦 ∈ 𝑌 ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
103 102 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝑌 ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
104 4 fvexi ⊢ 𝑌 ∈ V
105 nnenom ⊢ ℕ ≈ ω
106 oveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑛 ) → ( 𝐴 𝐷 𝑦 ) = ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) )
107 106 oveq1d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) = ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) )
108 107 breq1d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑛 ) → ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ↔ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
109 104 105 108 axcc4 ⊢ ( ∀ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝑌 ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑌 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
110 103 109 syl ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑌 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) )
111 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 𝑌 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ) → 𝑈 ∈ CPreHilOLD )
112 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 𝑌 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ) → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
113 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 𝑌 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ) → 𝐴 ∈ 𝑋 )
114 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 𝑌 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ) → 𝑓 : ℕ ⟶ 𝑌 )
115 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 𝑌 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ) → ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
116 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑘 ) )
117 116 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) = ( 𝐴 𝐷 ( 𝑓 ‘ 𝑘 ) ) )
118 117 oveq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) = ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑘 ) ) ↑ 2 ) )
119 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 1 / 𝑛 ) = ( 1 / 𝑘 ) )
120 119 oveq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) = ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑘 ) ) )
121 118 120 breq12d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ↔ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑘 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑘 ) ) ) )
122 121 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑘 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑘 ) ) )
123 115 122 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 𝑌 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑘 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑘 ) ) )
124 eqid ⊢ ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) = ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝑓 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) )
125 1 2 3 4 111 112 113 8 9 10 11 114 123 124 minvecolem4 ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ 𝑌 ∧ ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝑓 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ) ) → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
126 110 125 exlimddv ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )