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 |
|
minvec.p |
β’ π = βͺ ( π½ fLim ( π filGen πΉ ) ) |
14 |
|
minvec.t |
β’ π = ( ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) |
15 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
minveclem4a |
β’ ( π β π β ( ( π½ fLim ( π filGen πΉ ) ) β© π ) ) |
16 |
15
|
elin2d |
β’ ( π β π β π ) |
17 |
11
|
oveqi |
β’ ( π΄ π· π ) = ( π΄ ( ( dist β π ) βΎ ( π Γ π ) ) π ) |
18 |
1 2 3 4 5 6 7 8 9 10 11 12 13
|
minveclem4b |
β’ ( π β π β π ) |
19 |
7 18
|
ovresd |
β’ ( π β ( π΄ ( ( dist β π ) βΎ ( π Γ π ) ) π ) = ( π΄ ( dist β π ) π ) ) |
20 |
17 19
|
eqtrid |
β’ ( π β ( π΄ π· π ) = ( π΄ ( dist β π ) π ) ) |
21 |
|
cphngp |
β’ ( π β βPreHil β π β NrmGrp ) |
22 |
4 21
|
syl |
β’ ( π β π β NrmGrp ) |
23 |
|
eqid |
β’ ( dist β π ) = ( dist β π ) |
24 |
3 1 2 23
|
ngpds |
β’ ( ( π β NrmGrp β§ π΄ β π β§ π β π ) β ( π΄ ( dist β π ) π ) = ( π β ( π΄ β π ) ) ) |
25 |
22 7 18 24
|
syl3anc |
β’ ( π β ( π΄ ( dist β π ) π ) = ( π β ( π΄ β π ) ) ) |
26 |
20 25
|
eqtrd |
β’ ( π β ( π΄ π· π ) = ( π β ( π΄ β π ) ) ) |
27 |
26
|
adantr |
β’ ( ( π β§ π¦ β π ) β ( π΄ π· π ) = ( π β ( π΄ β π ) ) ) |
28 |
|
ngpms |
β’ ( π β NrmGrp β π β MetSp ) |
29 |
1 11
|
msmet |
β’ ( π β MetSp β π· β ( Met β π ) ) |
30 |
22 28 29
|
3syl |
β’ ( π β π· β ( Met β π ) ) |
31 |
|
metcl |
β’ ( ( π· β ( Met β π ) β§ π΄ β π β§ π β π ) β ( π΄ π· π ) β β ) |
32 |
30 7 18 31
|
syl3anc |
β’ ( π β ( π΄ π· π ) β β ) |
33 |
32
|
adantr |
β’ ( ( π β§ π¦ β π ) β ( π΄ π· π ) β β ) |
34 |
1 2 3 4 5 6 7 8 9 10
|
minveclem4c |
β’ ( π β π β β ) |
35 |
34
|
adantr |
β’ ( ( π β§ π¦ β π ) β π β β ) |
36 |
22
|
adantr |
β’ ( ( π β§ π¦ β π ) β π β NrmGrp ) |
37 |
|
cphlmod |
β’ ( π β βPreHil β π β LMod ) |
38 |
4 37
|
syl |
β’ ( π β π β LMod ) |
39 |
38
|
adantr |
β’ ( ( π β§ π¦ β π ) β π β LMod ) |
40 |
7
|
adantr |
β’ ( ( π β§ π¦ β π ) β π΄ β π ) |
41 |
|
eqid |
β’ ( LSubSp β π ) = ( LSubSp β π ) |
42 |
1 41
|
lssss |
β’ ( π β ( LSubSp β π ) β π β π ) |
43 |
5 42
|
syl |
β’ ( π β π β π ) |
44 |
43
|
sselda |
β’ ( ( π β§ π¦ β π ) β π¦ β π ) |
45 |
1 2
|
lmodvsubcl |
β’ ( ( π β LMod β§ π΄ β π β§ π¦ β π ) β ( π΄ β π¦ ) β π ) |
46 |
39 40 44 45
|
syl3anc |
β’ ( ( π β§ π¦ β π ) β ( π΄ β π¦ ) β π ) |
47 |
1 3
|
nmcl |
β’ ( ( π β NrmGrp β§ ( π΄ β π¦ ) β π ) β ( π β ( π΄ β π¦ ) ) β β ) |
48 |
36 46 47
|
syl2anc |
β’ ( ( π β§ π¦ β π ) β ( π β ( π΄ β π¦ ) ) β β ) |
49 |
34 32
|
ltnled |
β’ ( π β ( π < ( π΄ π· π ) β Β¬ ( π΄ π· π ) β€ π ) ) |
50 |
1 2 3 4 5 6 7 8 9 10 11 12
|
minveclem3b |
β’ ( π β πΉ β ( fBas β π ) ) |
51 |
|
fbsspw |
β’ ( πΉ β ( fBas β π ) β πΉ β π« π ) |
52 |
50 51
|
syl |
β’ ( π β πΉ β π« π ) |
53 |
43
|
sspwd |
β’ ( π β π« π β π« π ) |
54 |
52 53
|
sstrd |
β’ ( π β πΉ β π« π ) |
55 |
1
|
fvexi |
β’ π β V |
56 |
55
|
a1i |
β’ ( π β π β V ) |
57 |
|
fbasweak |
β’ ( ( πΉ β ( fBas β π ) β§ πΉ β π« π β§ π β V ) β πΉ β ( fBas β π ) ) |
58 |
50 54 56 57
|
syl3anc |
β’ ( π β πΉ β ( fBas β π ) ) |
59 |
58
|
adantr |
β’ ( ( π β§ π < ( π΄ π· π ) ) β πΉ β ( fBas β π ) ) |
60 |
|
fgcl |
β’ ( πΉ β ( fBas β π ) β ( π filGen πΉ ) β ( Fil β π ) ) |
61 |
59 60
|
syl |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( π filGen πΉ ) β ( Fil β π ) ) |
62 |
|
ssfg |
β’ ( πΉ β ( fBas β π ) β πΉ β ( π filGen πΉ ) ) |
63 |
59 62
|
syl |
β’ ( ( π β§ π < ( π΄ π· π ) ) β πΉ β ( π filGen πΉ ) ) |
64 |
32 34
|
readdcld |
β’ ( π β ( ( π΄ π· π ) + π ) β β ) |
65 |
64
|
rehalfcld |
β’ ( π β ( ( ( π΄ π· π ) + π ) / 2 ) β β ) |
66 |
65
|
resqcld |
β’ ( π β ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β β ) |
67 |
34
|
resqcld |
β’ ( π β ( π β 2 ) β β ) |
68 |
66 67
|
resubcld |
β’ ( π β ( ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) β β ) |
69 |
68
|
adantr |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) β β ) |
70 |
34 32 34
|
ltadd1d |
β’ ( π β ( π < ( π΄ π· π ) β ( π + π ) < ( ( π΄ π· π ) + π ) ) ) |
71 |
34
|
recnd |
β’ ( π β π β β ) |
72 |
71
|
2timesd |
β’ ( π β ( 2 Β· π ) = ( π + π ) ) |
73 |
72
|
breq1d |
β’ ( π β ( ( 2 Β· π ) < ( ( π΄ π· π ) + π ) β ( π + π ) < ( ( π΄ π· π ) + π ) ) ) |
74 |
|
2re |
β’ 2 β β |
75 |
|
2pos |
β’ 0 < 2 |
76 |
74 75
|
pm3.2i |
β’ ( 2 β β β§ 0 < 2 ) |
77 |
76
|
a1i |
β’ ( π β ( 2 β β β§ 0 < 2 ) ) |
78 |
|
ltmuldiv2 |
β’ ( ( π β β β§ ( ( π΄ π· π ) + π ) β β β§ ( 2 β β β§ 0 < 2 ) ) β ( ( 2 Β· π ) < ( ( π΄ π· π ) + π ) β π < ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
79 |
34 64 77 78
|
syl3anc |
β’ ( π β ( ( 2 Β· π ) < ( ( π΄ π· π ) + π ) β π < ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
80 |
70 73 79
|
3bitr2d |
β’ ( π β ( π < ( π΄ π· π ) β π < ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
81 |
1 2 3 4 5 6 7 8 9
|
minveclem1 |
β’ ( π β ( π
β β β§ π
β β
β§ β π€ β π
0 β€ π€ ) ) |
82 |
81
|
simp3d |
β’ ( π β β π€ β π
0 β€ π€ ) |
83 |
81
|
simp1d |
β’ ( π β π
β β ) |
84 |
81
|
simp2d |
β’ ( π β π
β β
) |
85 |
|
0re |
β’ 0 β β |
86 |
|
breq1 |
β’ ( π₯ = 0 β ( π₯ β€ π€ β 0 β€ π€ ) ) |
87 |
86
|
ralbidv |
β’ ( π₯ = 0 β ( β π€ β π
π₯ β€ π€ β β π€ β π
0 β€ π€ ) ) |
88 |
87
|
rspcev |
β’ ( ( 0 β β β§ β π€ β π
0 β€ π€ ) β β π₯ β β β π€ β π
π₯ β€ π€ ) |
89 |
85 82 88
|
sylancr |
β’ ( π β β π₯ β β β π€ β π
π₯ β€ π€ ) |
90 |
85
|
a1i |
β’ ( π β 0 β β ) |
91 |
|
infregelb |
β’ ( ( ( π
β β β§ π
β β
β§ β π₯ β β β π€ β π
π₯ β€ π€ ) β§ 0 β β ) β ( 0 β€ inf ( π
, β , < ) β β π€ β π
0 β€ π€ ) ) |
92 |
83 84 89 90 91
|
syl31anc |
β’ ( π β ( 0 β€ inf ( π
, β , < ) β β π€ β π
0 β€ π€ ) ) |
93 |
82 92
|
mpbird |
β’ ( π β 0 β€ inf ( π
, β , < ) ) |
94 |
93 10
|
breqtrrdi |
β’ ( π β 0 β€ π ) |
95 |
|
metge0 |
β’ ( ( π· β ( Met β π ) β§ π΄ β π β§ π β π ) β 0 β€ ( π΄ π· π ) ) |
96 |
30 7 18 95
|
syl3anc |
β’ ( π β 0 β€ ( π΄ π· π ) ) |
97 |
32 34 96 94
|
addge0d |
β’ ( π β 0 β€ ( ( π΄ π· π ) + π ) ) |
98 |
|
divge0 |
β’ ( ( ( ( ( π΄ π· π ) + π ) β β β§ 0 β€ ( ( π΄ π· π ) + π ) ) β§ ( 2 β β β§ 0 < 2 ) ) β 0 β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) |
99 |
64 97 77 98
|
syl21anc |
β’ ( π β 0 β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) |
100 |
34 65 94 99
|
lt2sqd |
β’ ( π β ( π < ( ( ( π΄ π· π ) + π ) / 2 ) β ( π β 2 ) < ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) ) ) |
101 |
67 66
|
posdifd |
β’ ( π β ( ( π β 2 ) < ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β 0 < ( ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) ) |
102 |
80 100 101
|
3bitrd |
β’ ( π β ( π < ( π΄ π· π ) β 0 < ( ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) ) |
103 |
102
|
biimpa |
β’ ( ( π β§ π < ( π΄ π· π ) ) β 0 < ( ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) |
104 |
69 103
|
elrpd |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) β β+ ) |
105 |
14 104
|
eqeltrid |
β’ ( ( π β§ π < ( π΄ π· π ) ) β π β β+ ) |
106 |
5
|
adantr |
β’ ( ( π β§ π < ( π΄ π· π ) ) β π β ( LSubSp β π ) ) |
107 |
|
rabexg |
β’ ( π β ( LSubSp β π ) β { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β V ) |
108 |
106 107
|
syl |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β V ) |
109 |
|
eqid |
β’ ( π β β+ β¦ { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } ) = ( π β β+ β¦ { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } ) |
110 |
|
oveq2 |
β’ ( π = π β ( ( π β 2 ) + π ) = ( ( π β 2 ) + π ) ) |
111 |
110
|
breq2d |
β’ ( π = π β ( ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) β ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) ) ) |
112 |
111
|
rabbidv |
β’ ( π = π β { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } = { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } ) |
113 |
109 112
|
elrnmpt1s |
β’ ( ( π β β+ β§ { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β V ) β { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β ran ( π β β+ β¦ { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } ) ) |
114 |
105 108 113
|
syl2anc |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β ran ( π β β+ β¦ { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } ) ) |
115 |
114 12
|
eleqtrrdi |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β πΉ ) |
116 |
63 115
|
sseldd |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β ( π filGen πΉ ) ) |
117 |
|
ssrab2 |
β’ { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β π |
118 |
117
|
a1i |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β π ) |
119 |
14
|
oveq2i |
β’ ( ( π β 2 ) + π ) = ( ( π β 2 ) + ( ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) |
120 |
67
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( π β 2 ) β β ) |
121 |
120
|
recnd |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( π β 2 ) β β ) |
122 |
65
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( ( ( π΄ π· π ) + π ) / 2 ) β β ) |
123 |
122
|
resqcld |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β β ) |
124 |
123
|
recnd |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β β ) |
125 |
121 124
|
pncan3d |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( ( π β 2 ) + ( ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) β ( π β 2 ) ) ) = ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) ) |
126 |
119 125
|
eqtrid |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( ( π β 2 ) + π ) = ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) ) |
127 |
126
|
breq2d |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) β ( ( π΄ π· π¦ ) β 2 ) β€ ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) ) ) |
128 |
30
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β π· β ( Met β π ) ) |
129 |
7
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β π΄ β π ) |
130 |
44
|
adantlr |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β π¦ β π ) |
131 |
|
metcl |
β’ ( ( π· β ( Met β π ) β§ π΄ β π β§ π¦ β π ) β ( π΄ π· π¦ ) β β ) |
132 |
128 129 130 131
|
syl3anc |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( π΄ π· π¦ ) β β ) |
133 |
|
metge0 |
β’ ( ( π· β ( Met β π ) β§ π΄ β π β§ π¦ β π ) β 0 β€ ( π΄ π· π¦ ) ) |
134 |
128 129 130 133
|
syl3anc |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β 0 β€ ( π΄ π· π¦ ) ) |
135 |
99
|
ad2antrr |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β 0 β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) |
136 |
132 122 134 135
|
le2sqd |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) β ( ( π΄ π· π¦ ) β 2 ) β€ ( ( ( ( π΄ π· π ) + π ) / 2 ) β 2 ) ) ) |
137 |
127 136
|
bitr4d |
β’ ( ( ( π β§ π < ( π΄ π· π ) ) β§ π¦ β π ) β ( ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) β ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
138 |
137
|
rabbidva |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } = { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) |
139 |
43
|
adantr |
β’ ( ( π β§ π < ( π΄ π· π ) ) β π β π ) |
140 |
|
rabss2 |
β’ ( π β π β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) |
141 |
139 140
|
syl |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) |
142 |
138 141
|
eqsstrd |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) |
143 |
|
filss |
β’ ( ( ( π filGen πΉ ) β ( Fil β π ) β§ ( { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β ( π filGen πΉ ) β§ { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β π β§ { π¦ β π β£ ( ( π΄ π· π¦ ) β 2 ) β€ ( ( π β 2 ) + π ) } β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β ( π filGen πΉ ) ) |
144 |
61 116 118 142 143
|
syl13anc |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β ( π filGen πΉ ) ) |
145 |
|
flimclsi |
β’ ( { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β ( π filGen πΉ ) β ( π½ fLim ( π filGen πΉ ) ) β ( ( cls β π½ ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) ) |
146 |
144 145
|
syl |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( π½ fLim ( π filGen πΉ ) ) β ( ( cls β π½ ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) ) |
147 |
15
|
elin1d |
β’ ( π β π β ( π½ fLim ( π filGen πΉ ) ) ) |
148 |
147
|
adantr |
β’ ( ( π β§ π < ( π΄ π· π ) ) β π β ( π½ fLim ( π filGen πΉ ) ) ) |
149 |
146 148
|
sseldd |
β’ ( ( π β§ π < ( π΄ π· π ) ) β π β ( ( cls β π½ ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) ) |
150 |
|
ngpxms |
β’ ( π β NrmGrp β π β βMetSp ) |
151 |
1 11
|
xmsxmet |
β’ ( π β βMetSp β π· β ( βMet β π ) ) |
152 |
22 150 151
|
3syl |
β’ ( π β π· β ( βMet β π ) ) |
153 |
152
|
adantr |
β’ ( ( π β§ π < ( π΄ π· π ) ) β π· β ( βMet β π ) ) |
154 |
7
|
adantr |
β’ ( ( π β§ π < ( π΄ π· π ) ) β π΄ β π ) |
155 |
65
|
adantr |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( ( ( π΄ π· π ) + π ) / 2 ) β β ) |
156 |
155
|
rexrd |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( ( ( π΄ π· π ) + π ) / 2 ) β β* ) |
157 |
|
eqid |
β’ ( MetOpen β π· ) = ( MetOpen β π· ) |
158 |
|
eqid |
β’ { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } = { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } |
159 |
157 158
|
blcld |
β’ ( ( π· β ( βMet β π ) β§ π΄ β π β§ ( ( ( π΄ π· π ) + π ) / 2 ) β β* ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β ( Clsd β ( MetOpen β π· ) ) ) |
160 |
153 154 156 159
|
syl3anc |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β ( Clsd β ( MetOpen β π· ) ) ) |
161 |
8 1 11
|
xmstopn |
β’ ( π β βMetSp β π½ = ( MetOpen β π· ) ) |
162 |
22 150 161
|
3syl |
β’ ( π β π½ = ( MetOpen β π· ) ) |
163 |
162
|
adantr |
β’ ( ( π β§ π < ( π΄ π· π ) ) β π½ = ( MetOpen β π· ) ) |
164 |
163
|
fveq2d |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( Clsd β π½ ) = ( Clsd β ( MetOpen β π· ) ) ) |
165 |
160 164
|
eleqtrrd |
β’ ( ( π β§ π < ( π΄ π· π ) ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β ( Clsd β π½ ) ) |
166 |
|
cldcls |
β’ ( { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β ( Clsd β π½ ) β ( ( cls β π½ ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) = { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) |
167 |
165 166
|
syl |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( ( cls β π½ ) β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) = { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) |
168 |
149 167
|
eleqtrd |
β’ ( ( π β§ π < ( π΄ π· π ) ) β π β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } ) |
169 |
|
oveq2 |
β’ ( π¦ = π β ( π΄ π· π¦ ) = ( π΄ π· π ) ) |
170 |
169
|
breq1d |
β’ ( π¦ = π β ( ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) β ( π΄ π· π ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
171 |
170
|
elrab |
β’ ( π β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β ( π β π β§ ( π΄ π· π ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
172 |
171
|
simprbi |
β’ ( π β { π¦ β π β£ ( π΄ π· π¦ ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) } β ( π΄ π· π ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) |
173 |
168 172
|
syl |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( π΄ π· π ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) |
174 |
32 34 32
|
leadd2d |
β’ ( π β ( ( π΄ π· π ) β€ π β ( ( π΄ π· π ) + ( π΄ π· π ) ) β€ ( ( π΄ π· π ) + π ) ) ) |
175 |
32
|
recnd |
β’ ( π β ( π΄ π· π ) β β ) |
176 |
175
|
2timesd |
β’ ( π β ( 2 Β· ( π΄ π· π ) ) = ( ( π΄ π· π ) + ( π΄ π· π ) ) ) |
177 |
176
|
breq1d |
β’ ( π β ( ( 2 Β· ( π΄ π· π ) ) β€ ( ( π΄ π· π ) + π ) β ( ( π΄ π· π ) + ( π΄ π· π ) ) β€ ( ( π΄ π· π ) + π ) ) ) |
178 |
|
lemuldiv2 |
β’ ( ( ( π΄ π· π ) β β β§ ( ( π΄ π· π ) + π ) β β β§ ( 2 β β β§ 0 < 2 ) ) β ( ( 2 Β· ( π΄ π· π ) ) β€ ( ( π΄ π· π ) + π ) β ( π΄ π· π ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
179 |
76 178
|
mp3an3 |
β’ ( ( ( π΄ π· π ) β β β§ ( ( π΄ π· π ) + π ) β β ) β ( ( 2 Β· ( π΄ π· π ) ) β€ ( ( π΄ π· π ) + π ) β ( π΄ π· π ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
180 |
32 64 179
|
syl2anc |
β’ ( π β ( ( 2 Β· ( π΄ π· π ) ) β€ ( ( π΄ π· π ) + π ) β ( π΄ π· π ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
181 |
174 177 180
|
3bitr2d |
β’ ( π β ( ( π΄ π· π ) β€ π β ( π΄ π· π ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) ) |
182 |
181
|
biimpar |
β’ ( ( π β§ ( π΄ π· π ) β€ ( ( ( π΄ π· π ) + π ) / 2 ) ) β ( π΄ π· π ) β€ π ) |
183 |
173 182
|
syldan |
β’ ( ( π β§ π < ( π΄ π· π ) ) β ( π΄ π· π ) β€ π ) |
184 |
183
|
ex |
β’ ( π β ( π < ( π΄ π· π ) β ( π΄ π· π ) β€ π ) ) |
185 |
49 184
|
sylbird |
β’ ( π β ( Β¬ ( π΄ π· π ) β€ π β ( π΄ π· π ) β€ π ) ) |
186 |
185
|
pm2.18d |
β’ ( π β ( π΄ π· π ) β€ π ) |
187 |
186
|
adantr |
β’ ( ( π β§ π¦ β π ) β ( π΄ π· π ) β€ π ) |
188 |
83
|
adantr |
β’ ( ( π β§ π¦ β π ) β π
β β ) |
189 |
89
|
adantr |
β’ ( ( π β§ π¦ β π ) β β π₯ β β β π€ β π
π₯ β€ π€ ) |
190 |
|
simpr |
β’ ( ( π β§ π¦ β π ) β π¦ β π ) |
191 |
|
fvex |
β’ ( π β ( π΄ β π¦ ) ) β V |
192 |
|
eqid |
β’ ( π¦ β π β¦ ( π β ( π΄ β π¦ ) ) ) = ( π¦ β π β¦ ( π β ( π΄ β π¦ ) ) ) |
193 |
192
|
elrnmpt1 |
β’ ( ( π¦ β π β§ ( π β ( π΄ β π¦ ) ) β V ) β ( π β ( π΄ β π¦ ) ) β ran ( π¦ β π β¦ ( π β ( π΄ β π¦ ) ) ) ) |
194 |
190 191 193
|
sylancl |
β’ ( ( π β§ π¦ β π ) β ( π β ( π΄ β π¦ ) ) β ran ( π¦ β π β¦ ( π β ( π΄ β π¦ ) ) ) ) |
195 |
194 9
|
eleqtrrdi |
β’ ( ( π β§ π¦ β π ) β ( π β ( π΄ β π¦ ) ) β π
) |
196 |
|
infrelb |
β’ ( ( π
β β β§ β π₯ β β β π€ β π
π₯ β€ π€ β§ ( π β ( π΄ β π¦ ) ) β π
) β inf ( π
, β , < ) β€ ( π β ( π΄ β π¦ ) ) ) |
197 |
188 189 195 196
|
syl3anc |
β’ ( ( π β§ π¦ β π ) β inf ( π
, β , < ) β€ ( π β ( π΄ β π¦ ) ) ) |
198 |
10 197
|
eqbrtrid |
β’ ( ( π β§ π¦ β π ) β π β€ ( π β ( π΄ β π¦ ) ) ) |
199 |
33 35 48 187 198
|
letrd |
β’ ( ( π β§ π¦ β π ) β ( π΄ π· π ) β€ ( π β ( π΄ β π¦ ) ) ) |
200 |
27 199
|
eqbrtrrd |
β’ ( ( π β§ π¦ β π ) β ( π β ( π΄ β π ) ) β€ ( π β ( π΄ β π¦ ) ) ) |
201 |
200
|
ralrimiva |
β’ ( π β β π¦ β π ( π β ( π΄ β π ) ) β€ ( π β ( π΄ β π¦ ) ) ) |
202 |
|
oveq2 |
β’ ( π₯ = π β ( π΄ β π₯ ) = ( π΄ β π ) ) |
203 |
202
|
fveq2d |
β’ ( π₯ = π β ( π β ( π΄ β π₯ ) ) = ( π β ( π΄ β π ) ) ) |
204 |
203
|
breq1d |
β’ ( π₯ = π β ( ( π β ( π΄ β π₯ ) ) β€ ( π β ( π΄ β π¦ ) ) β ( π β ( π΄ β π ) ) β€ ( π β ( π΄ β π¦ ) ) ) ) |
205 |
204
|
ralbidv |
β’ ( π₯ = π β ( β π¦ β π ( π β ( π΄ β π₯ ) ) β€ ( π β ( π΄ β π¦ ) ) β β π¦ β π ( π β ( π΄ β π ) ) β€ ( π β ( π΄ β π¦ ) ) ) ) |
206 |
205
|
rspcev |
β’ ( ( π β π β§ β π¦ β π ( π β ( π΄ β π ) ) β€ ( π β ( π΄ β π¦ ) ) ) β β π₯ β π β π¦ β π ( π β ( π΄ β π₯ ) ) β€ ( π β ( π΄ β π¦ ) ) ) |
207 |
16 201 206
|
syl2anc |
β’ ( π β β π₯ β π β π¦ β π ( π β ( π΄ β π₯ ) ) β€ ( π β ( π΄ β π¦ ) ) ) |