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 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
minveco.m ${⊢}{M}={-}_{v}\left({U}\right)$
minveco.n ${⊢}{N}={norm}_{CV}\left({U}\right)$
minveco.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
minveco.u ${⊢}{\phi }\to {U}\in {CPreHil}_{\mathrm{OLD}}$
minveco.w ${⊢}{\phi }\to {W}\in \left(\mathrm{SubSp}\left({U}\right)\cap \mathrm{CBan}\right)$
minveco.a ${⊢}{\phi }\to {A}\in {X}$
minveco.d ${⊢}{D}=\mathrm{IndMet}\left({U}\right)$
minveco.j ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
minveco.r ${⊢}{R}=\mathrm{ran}\left({y}\in {Y}⟼{N}\left({A}{M}{y}\right)\right)$
minveco.s ${⊢}{S}=sup\left({R},ℝ,<\right)$
Assertion minvecolem5 ${⊢}{\phi }\to \exists {x}\in {Y}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{N}\left({A}{M}{x}\right)\le {N}\left({A}{M}{y}\right)$

Proof

Step Hyp Ref Expression
1 minveco.x ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 minveco.m ${⊢}{M}={-}_{v}\left({U}\right)$
3 minveco.n ${⊢}{N}={norm}_{CV}\left({U}\right)$
4 minveco.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
5 minveco.u ${⊢}{\phi }\to {U}\in {CPreHil}_{\mathrm{OLD}}$
6 minveco.w ${⊢}{\phi }\to {W}\in \left(\mathrm{SubSp}\left({U}\right)\cap \mathrm{CBan}\right)$
7 minveco.a ${⊢}{\phi }\to {A}\in {X}$
8 minveco.d ${⊢}{D}=\mathrm{IndMet}\left({U}\right)$
9 minveco.j ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
10 minveco.r ${⊢}{R}=\mathrm{ran}\left({y}\in {Y}⟼{N}\left({A}{M}{y}\right)\right)$
11 minveco.s ${⊢}{S}=sup\left({R},ℝ,<\right)$
12 nnrecgt0 ${⊢}{n}\in ℕ\to 0<\frac{1}{{n}}$
13 12 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 0<\frac{1}{{n}}$
14 nnrecre ${⊢}{n}\in ℕ\to \frac{1}{{n}}\in ℝ$
15 14 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{1}{{n}}\in ℝ$
16 1 2 3 4 5 6 7 8 9 10 minvecolem1 ${⊢}{\phi }\to \left({R}\subseteq ℝ\wedge {R}\ne \varnothing \wedge \forall {w}\in {R}\phantom{\rule{.4em}{0ex}}0\le {w}\right)$
17 16 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({R}\subseteq ℝ\wedge {R}\ne \varnothing \wedge \forall {w}\in {R}\phantom{\rule{.4em}{0ex}}0\le {w}\right)$
18 17 simp1d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {R}\subseteq ℝ$
19 17 simp2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {R}\ne \varnothing$
20 0re ${⊢}0\in ℝ$
21 17 simp3d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \forall {w}\in {R}\phantom{\rule{.4em}{0ex}}0\le {w}$
22 breq1 ${⊢}{x}=0\to \left({x}\le {w}↔0\le {w}\right)$
23 22 ralbidv ${⊢}{x}=0\to \left(\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}{x}\le {w}↔\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}0\le {w}\right)$
24 23 rspcev ${⊢}\left(0\in ℝ\wedge \forall {w}\in {R}\phantom{\rule{.4em}{0ex}}0\le {w}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}{x}\le {w}$
25 20 21 24 sylancr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}{x}\le {w}$
26 infrecl ${⊢}\left({R}\subseteq ℝ\wedge {R}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}{x}\le {w}\right)\to sup\left({R},ℝ,<\right)\in ℝ$
27 18 19 25 26 syl3anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to sup\left({R},ℝ,<\right)\in ℝ$
28 11 27 eqeltrid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {S}\in ℝ$
29 28 resqcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{S}}^{2}\in ℝ$
30 15 29 ltaddposd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(0<\frac{1}{{n}}↔{{S}}^{2}<{{S}}^{2}+\left(\frac{1}{{n}}\right)\right)$
31 13 30 mpbid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{S}}^{2}<{{S}}^{2}+\left(\frac{1}{{n}}\right)$
32 29 15 readdcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{S}}^{2}+\left(\frac{1}{{n}}\right)\in ℝ$
33 28 sqge0d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 0\le {{S}}^{2}$
34 29 15 33 13 addgegt0d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 0<{{S}}^{2}+\left(\frac{1}{{n}}\right)$
35 32 34 elrpd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{S}}^{2}+\left(\frac{1}{{n}}\right)\in {ℝ}^{+}$
36 35 rpge0d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 0\le {{S}}^{2}+\left(\frac{1}{{n}}\right)$
37 resqrtth ${⊢}\left({{S}}^{2}+\left(\frac{1}{{n}}\right)\in ℝ\wedge 0\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)\to {\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}}^{2}={{S}}^{2}+\left(\frac{1}{{n}}\right)$
38 32 36 37 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}}^{2}={{S}}^{2}+\left(\frac{1}{{n}}\right)$
39 31 38 breqtrrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {{S}}^{2}<{\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}}^{2}$
40 35 rpsqrtcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\in {ℝ}^{+}$
41 40 rpred ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\in ℝ$
42 0red ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 0\in ℝ$
43 infregelb ${⊢}\left(\left({R}\subseteq ℝ\wedge {R}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}{x}\le {w}\right)\wedge 0\in ℝ\right)\to \left(0\le sup\left({R},ℝ,<\right)↔\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}0\le {w}\right)$
44 18 19 25 42 43 syl31anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(0\le sup\left({R},ℝ,<\right)↔\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}0\le {w}\right)$
45 21 44 mpbird ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 0\le sup\left({R},ℝ,<\right)$
46 45 11 breqtrrdi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 0\le {S}$
47 32 36 sqrtge0d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to 0\le \sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}$
48 28 41 46 47 lt2sqd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({S}<\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}↔{{S}}^{2}<{\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}}^{2}\right)$
49 39 48 mpbird ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {S}<\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}$
50 28 41 ltnled ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({S}<\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}↔¬\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {S}\right)$
51 49 50 mpbid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to ¬\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {S}$
52 11 breq2i ${⊢}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {S}↔\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le sup\left({R},ℝ,<\right)$
53 infregelb ${⊢}\left(\left({R}\subseteq ℝ\wedge {R}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}{x}\le {w}\right)\wedge \sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\in ℝ\right)\to \left(\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le sup\left({R},ℝ,<\right)↔\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {w}\right)$
54 18 19 25 41 53 syl31anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le sup\left({R},ℝ,<\right)↔\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {w}\right)$
55 52 54 syl5bb ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {S}↔\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {w}\right)$
56 10 raleqi ${⊢}\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {w}↔\forall {w}\in \mathrm{ran}\left({y}\in {Y}⟼{N}\left({A}{M}{y}\right)\right)\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {w}$
57 fvex ${⊢}{N}\left({A}{M}{y}\right)\in \mathrm{V}$
58 57 rgenw ${⊢}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{N}\left({A}{M}{y}\right)\in \mathrm{V}$
59 eqid ${⊢}\left({y}\in {Y}⟼{N}\left({A}{M}{y}\right)\right)=\left({y}\in {Y}⟼{N}\left({A}{M}{y}\right)\right)$
60 breq2 ${⊢}{w}={N}\left({A}{M}{y}\right)\to \left(\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {w}↔\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)\right)$
61 59 60 ralrnmptw ${⊢}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{N}\left({A}{M}{y}\right)\in \mathrm{V}\to \left(\forall {w}\in \mathrm{ran}\left({y}\in {Y}⟼{N}\left({A}{M}{y}\right)\right)\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {w}↔\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)\right)$
62 58 61 ax-mp ${⊢}\forall {w}\in \mathrm{ran}\left({y}\in {Y}⟼{N}\left({A}{M}{y}\right)\right)\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {w}↔\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)$
63 56 62 bitri ${⊢}\forall {w}\in {R}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {w}↔\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)$
64 55 63 syl6bb ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {S}↔\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)\right)$
65 51 64 mtbid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to ¬\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)$
66 rexnal ${⊢}\exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}¬\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)↔¬\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)$
67 65 66 sylibr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}¬\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)$
68 32 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {{S}}^{2}+\left(\frac{1}{{n}}\right)\in ℝ$
69 phnv ${⊢}{U}\in {CPreHil}_{\mathrm{OLD}}\to {U}\in \mathrm{NrmCVec}$
70 5 69 syl ${⊢}{\phi }\to {U}\in \mathrm{NrmCVec}$
71 70 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {U}\in \mathrm{NrmCVec}$
72 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {A}\in {X}$
73 inss1 ${⊢}\mathrm{SubSp}\left({U}\right)\cap \mathrm{CBan}\subseteq \mathrm{SubSp}\left({U}\right)$
74 73 6 sseldi ${⊢}{\phi }\to {W}\in \mathrm{SubSp}\left({U}\right)$
75 eqid ${⊢}\mathrm{SubSp}\left({U}\right)=\mathrm{SubSp}\left({U}\right)$
76 1 4 75 sspba ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{SubSp}\left({U}\right)\right)\to {Y}\subseteq {X}$
77 70 74 76 syl2anc ${⊢}{\phi }\to {Y}\subseteq {X}$
78 77 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {Y}\subseteq {X}$
79 78 sselda ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {y}\in {X}$
80 1 2 nvmcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {y}\in {X}\right)\to {A}{M}{y}\in {X}$
81 71 72 79 80 syl3anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {A}{M}{y}\in {X}$
82 1 3 nvcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}{M}{y}\in {X}\right)\to {N}\left({A}{M}{y}\right)\in ℝ$
83 71 81 82 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {N}\left({A}{M}{y}\right)\in ℝ$
84 83 resqcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {{N}\left({A}{M}{y}\right)}^{2}\in ℝ$
85 68 84 letrid ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to \left({{S}}^{2}+\left(\frac{1}{{n}}\right)\le {{N}\left({A}{M}{y}\right)}^{2}\vee {{N}\left({A}{M}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)$
86 85 ord ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to \left(¬{{S}}^{2}+\left(\frac{1}{{n}}\right)\le {{N}\left({A}{M}{y}\right)}^{2}\to {{N}\left({A}{M}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)$
87 41 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to \sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\in ℝ$
88 47 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to 0\le \sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}$
89 1 3 nvge0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}{M}{y}\in {X}\right)\to 0\le {N}\left({A}{M}{y}\right)$
90 71 81 89 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to 0\le {N}\left({A}{M}{y}\right)$
91 87 83 88 90 le2sqd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to \left(\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)↔{\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}}^{2}\le {{N}\left({A}{M}{y}\right)}^{2}\right)$
92 38 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}}^{2}={{S}}^{2}+\left(\frac{1}{{n}}\right)$
93 92 breq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to \left({\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}}^{2}\le {{N}\left({A}{M}{y}\right)}^{2}↔{{S}}^{2}+\left(\frac{1}{{n}}\right)\le {{N}\left({A}{M}{y}\right)}^{2}\right)$
94 91 93 bitrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to \left(\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)↔{{S}}^{2}+\left(\frac{1}{{n}}\right)\le {{N}\left({A}{M}{y}\right)}^{2}\right)$
95 94 notbid ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to \left(¬\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)↔¬{{S}}^{2}+\left(\frac{1}{{n}}\right)\le {{N}\left({A}{M}{y}\right)}^{2}\right)$
96 1 2 3 8 imsdval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {y}\in {X}\right)\to {A}{D}{y}={N}\left({A}{M}{y}\right)$
97 71 72 79 96 syl3anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {A}{D}{y}={N}\left({A}{M}{y}\right)$
98 97 oveq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to {\left({A}{D}{y}\right)}^{2}={{N}\left({A}{M}{y}\right)}^{2}$
99 98 breq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to \left({\left({A}{D}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)↔{{N}\left({A}{M}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)$
100 86 95 99 3imtr4d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in {Y}\right)\to \left(¬\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)\to {\left({A}{D}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)$
101 100 reximdva ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}¬\sqrt{{{S}}^{2}+\left(\frac{1}{{n}}\right)}\le {N}\left({A}{M}{y}\right)\to \exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}{\left({A}{D}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)$
102 67 101 mpd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}{\left({A}{D}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)$
103 102 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}{\left({A}{D}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)$
104 4 fvexi ${⊢}{Y}\in \mathrm{V}$
105 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
106 oveq2 ${⊢}{y}={f}\left({n}\right)\to {A}{D}{y}={A}{D}{f}\left({n}\right)$
107 106 oveq1d ${⊢}{y}={f}\left({n}\right)\to {\left({A}{D}{y}\right)}^{2}={\left({A}{D}{f}\left({n}\right)\right)}^{2}$
108 107 breq1d ${⊢}{y}={f}\left({n}\right)\to \left({\left({A}{D}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)↔{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)$
109 104 105 108 axcc4 ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in {Y}\phantom{\rule{.4em}{0ex}}{\left({A}{D}{y}\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{Y}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)$
110 103 109 syl ${⊢}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{Y}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)$
111 5 adantr ${⊢}\left({\phi }\wedge \left({f}:ℕ⟶{Y}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)\right)\to {U}\in {CPreHil}_{\mathrm{OLD}}$
112 6 adantr ${⊢}\left({\phi }\wedge \left({f}:ℕ⟶{Y}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)\right)\to {W}\in \left(\mathrm{SubSp}\left({U}\right)\cap \mathrm{CBan}\right)$
113 7 adantr ${⊢}\left({\phi }\wedge \left({f}:ℕ⟶{Y}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)\right)\to {A}\in {X}$
114 simprl ${⊢}\left({\phi }\wedge \left({f}:ℕ⟶{Y}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)\right)\to {f}:ℕ⟶{Y}$
115 simprr ${⊢}\left({\phi }\wedge \left({f}:ℕ⟶{Y}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)$
116 fveq2 ${⊢}{n}={k}\to {f}\left({n}\right)={f}\left({k}\right)$
117 116 oveq2d ${⊢}{n}={k}\to {A}{D}{f}\left({n}\right)={A}{D}{f}\left({k}\right)$
118 117 oveq1d ${⊢}{n}={k}\to {\left({A}{D}{f}\left({n}\right)\right)}^{2}={\left({A}{D}{f}\left({k}\right)\right)}^{2}$
119 oveq2 ${⊢}{n}={k}\to \frac{1}{{n}}=\frac{1}{{k}}$
120 119 oveq2d ${⊢}{n}={k}\to {{S}}^{2}+\left(\frac{1}{{n}}\right)={{S}}^{2}+\left(\frac{1}{{k}}\right)$
121 118 120 breq12d ${⊢}{n}={k}\to \left({\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)↔{\left({A}{D}{f}\left({k}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{k}}\right)\right)$
122 121 rspccva ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\wedge {k}\in ℕ\right)\to {\left({A}{D}{f}\left({k}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{k}}\right)$
123 115 122 sylan ${⊢}\left(\left({\phi }\wedge \left({f}:ℕ⟶{Y}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)\right)\wedge {k}\in ℕ\right)\to {\left({A}{D}{f}\left({k}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{k}}\right)$
124 eqid
125 1 2 3 4 111 112 113 8 9 10 11 114 123 124 minvecolem4 ${⊢}\left({\phi }\wedge \left({f}:ℕ⟶{Y}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\left({A}{D}{f}\left({n}\right)\right)}^{2}\le {{S}}^{2}+\left(\frac{1}{{n}}\right)\right)\right)\to \exists {x}\in {Y}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{N}\left({A}{M}{x}\right)\le {N}\left({A}{M}{y}\right)$
126 110 125 exlimddv ${⊢}{\phi }\to \exists {x}\in {Y}\phantom{\rule{.4em}{0ex}}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}{N}\left({A}{M}{x}\right)\le {N}\left({A}{M}{y}\right)$