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 = BaseSet U
minveco.m M = - v U
minveco.n N = norm CV U
minveco.y Y = BaseSet W
minveco.u φ U CPreHil OLD
minveco.w φ W SubSp U CBan
minveco.a φ A X
minveco.d D = IndMet U
minveco.j J = MetOpen D
minveco.r R = ran y Y N A M y
minveco.s S = sup R <
Assertion minvecolem5 φ x Y y Y N A M x N A M y

Proof

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