Step | Hyp | Ref
| Expression |
1 | | rzal 4471 |
. . . . . . . . 9
β’ (π = β
β βπ‘ β π (πβ(π‘βπ§)) β€ π) |
2 | 1 | ralrimivw 3148 |
. . . . . . . 8
β’ (π = β
β βπ§ β π βπ‘ β π (πβ(π‘βπ§)) β€ π) |
3 | | rabid2 3439 |
. . . . . . . 8
β’ (π = {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π} β βπ§ β π βπ‘ β π (πβ(π‘βπ§)) β€ π) |
4 | 2, 3 | sylibr 233 |
. . . . . . 7
β’ (π = β
β π = {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) |
5 | 4 | eqcomd 2743 |
. . . . . 6
β’ (π = β
β {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π} = π) |
6 | 5 | eleq1d 2823 |
. . . . 5
β’ (π = β
β ({π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π} β (Clsdβπ½) β π β (Clsdβπ½))) |
7 | | iinrab 5034 |
. . . . . . 7
β’ (π β β
β β© π‘ β π {π§ β π β£ (πβ(π‘βπ§)) β€ π} = {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) |
8 | 7 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ π β β
) β β© π‘ β π {π§ β π β£ (πβ(π‘βπ§)) β€ π} = {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) |
9 | | id 22 |
. . . . . . 7
β’ (π β β
β π β β
) |
10 | | ubthlem.7 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β (π BLnOp π)) |
11 | 10 | sselda 3949 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π‘ β π) β π‘ β (π BLnOp π)) |
12 | | ubthlem.3 |
. . . . . . . . . . . . . . . . . . . 20
β’ π· = (IndMetβπ) |
13 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’
(IndMetβπ) =
(IndMetβπ) |
14 | | ubthlem.4 |
. . . . . . . . . . . . . . . . . . . 20
β’ π½ = (MetOpenβπ·) |
15 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’
(MetOpenβ(IndMetβπ)) = (MetOpenβ(IndMetβπ)) |
16 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π BLnOp π) = (π BLnOp π) |
17 | | ubthlem.5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β CBan |
18 | | bnnv 29850 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β CBan β π β
NrmCVec) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β NrmCVec |
20 | | ubthlem.6 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β NrmCVec |
21 | 12, 13, 14, 15, 16, 19, 20 | blocn2 29792 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ β (π BLnOp π) β π‘ β (π½ Cn (MetOpenβ(IndMetβπ)))) |
22 | | ubth.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ π = (BaseSetβπ) |
23 | 22, 12 | cbncms 29849 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β CBan β π· β (CMetβπ)) |
24 | 17, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π· β (CMetβπ) |
25 | | cmetmet 24666 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
26 | | metxmet 23703 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
27 | 24, 25, 26 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π· β (βMetβπ) |
28 | 14 | mopntopon 23808 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ π½ β (TopOnβπ) |
30 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(BaseSetβπ) =
(BaseSetβπ) |
31 | 30, 13 | imsxmet 29676 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β NrmCVec β
(IndMetβπ) β
(βMetβ(BaseSetβπ))) |
32 | 20, 31 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(IndMetβπ)
β (βMetβ(BaseSetβπ)) |
33 | 15 | mopntopon 23808 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((IndMetβπ)
β (βMetβ(BaseSetβπ)) β (MetOpenβ(IndMetβπ)) β
(TopOnβ(BaseSetβπ))) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’
(MetOpenβ(IndMetβπ)) β (TopOnβ(BaseSetβπ)) |
35 | | iscncl 22636 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β (TopOnβπ) β§
(MetOpenβ(IndMetβπ)) β (TopOnβ(BaseSetβπ))) β (π‘ β (π½ Cn (MetOpenβ(IndMetβπ))) β (π‘:πβΆ(BaseSetβπ) β§ βπ₯ β
(Clsdβ(MetOpenβ(IndMetβπ)))(β‘π‘ β π₯) β (Clsdβπ½)))) |
36 | 29, 34, 35 | mp2an 691 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ β (π½ Cn (MetOpenβ(IndMetβπ))) β (π‘:πβΆ(BaseSetβπ) β§ βπ₯ β
(Clsdβ(MetOpenβ(IndMetβπ)))(β‘π‘ β π₯) β (Clsdβπ½))) |
37 | 21, 36 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β (π BLnOp π) β (π‘:πβΆ(BaseSetβπ) β§ βπ₯ β
(Clsdβ(MetOpenβ(IndMetβπ)))(β‘π‘ β π₯) β (Clsdβπ½))) |
38 | 11, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π‘ β π) β (π‘:πβΆ(BaseSetβπ) β§ βπ₯ β
(Clsdβ(MetOpenβ(IndMetβπ)))(β‘π‘ β π₯) β (Clsdβπ½))) |
39 | 38 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π‘ β π) β π‘:πβΆ(BaseSetβπ)) |
40 | 39 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π‘ β π) β π‘:πβΆ(BaseSetβπ)) |
41 | 40 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π‘ β π) β§ π₯ β π) β (π‘βπ₯) β (BaseSetβπ)) |
42 | 41 | biantrurd 534 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ π‘ β π) β§ π₯ β π) β ((πβ(π‘βπ₯)) β€ π β ((π‘βπ₯) β (BaseSetβπ) β§ (πβ(π‘βπ₯)) β€ π))) |
43 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π‘βπ₯) β (πβπ¦) = (πβ(π‘βπ₯))) |
44 | 43 | breq1d 5120 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π‘βπ₯) β ((πβπ¦) β€ π β (πβ(π‘βπ₯)) β€ π)) |
45 | 44 | elrab 3650 |
. . . . . . . . . . . . 13
β’ ((π‘βπ₯) β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π} β ((π‘βπ₯) β (BaseSetβπ) β§ (πβ(π‘βπ₯)) β€ π)) |
46 | 42, 45 | bitr4di 289 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ π‘ β π) β§ π₯ β π) β ((πβ(π‘βπ₯)) β€ π β (π‘βπ₯) β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π})) |
47 | 46 | pm5.32da 580 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π‘ β π) β ((π₯ β π β§ (πβ(π‘βπ₯)) β€ π) β (π₯ β π β§ (π‘βπ₯) β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π}))) |
48 | | 2fveq3 6852 |
. . . . . . . . . . . . . 14
β’ (π§ = π₯ β (πβ(π‘βπ§)) = (πβ(π‘βπ₯))) |
49 | 48 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (π§ = π₯ β ((πβ(π‘βπ§)) β€ π β (πβ(π‘βπ₯)) β€ π)) |
50 | 49 | elrab 3650 |
. . . . . . . . . . . 12
β’ (π₯ β {π§ β π β£ (πβ(π‘βπ§)) β€ π} β (π₯ β π β§ (πβ(π‘βπ₯)) β€ π)) |
51 | 50 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π‘ β π) β (π₯ β {π§ β π β£ (πβ(π‘βπ§)) β€ π} β (π₯ β π β§ (πβ(π‘βπ₯)) β€ π))) |
52 | | ffn 6673 |
. . . . . . . . . . . 12
β’ (π‘:πβΆ(BaseSetβπ) β π‘ Fn π) |
53 | | elpreima 7013 |
. . . . . . . . . . . 12
β’ (π‘ Fn π β (π₯ β (β‘π‘ β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π}) β (π₯ β π β§ (π‘βπ₯) β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π}))) |
54 | 40, 52, 53 | 3syl 18 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π‘ β π) β (π₯ β (β‘π‘ β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π}) β (π₯ β π β§ (π‘βπ₯) β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π}))) |
55 | 47, 51, 54 | 3bitr4d 311 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π‘ β π) β (π₯ β {π§ β π β£ (πβ(π‘βπ§)) β€ π} β π₯ β (β‘π‘ β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π}))) |
56 | 55 | eqrdv 2735 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π‘ β π) β {π§ β π β£ (πβ(π‘βπ§)) β€ π} = (β‘π‘ β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π})) |
57 | | imaeq2 6014 |
. . . . . . . . . . 11
β’ (π₯ = {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π} β (β‘π‘ β π₯) = (β‘π‘ β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π})) |
58 | 57 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π₯ = {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π} β ((β‘π‘ β π₯) β (Clsdβπ½) β (β‘π‘ β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π}) β (Clsdβπ½))) |
59 | 38 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β βπ₯ β
(Clsdβ(MetOpenβ(IndMetβπ)))(β‘π‘ β π₯) β (Clsdβπ½)) |
60 | 59 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π‘ β π) β βπ₯ β
(Clsdβ(MetOpenβ(IndMetβπ)))(β‘π‘ β π₯) β (Clsdβπ½)) |
61 | | nnre 12167 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
62 | 61 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π‘ β π) β π β β) |
63 | 62 | rexrd 11212 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π‘ β π) β π β β*) |
64 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(0vecβπ) = (0vecβπ) |
65 | 30, 64 | nvzcl 29618 |
. . . . . . . . . . . . 13
β’ (π β NrmCVec β
(0vecβπ)
β (BaseSetβπ)) |
66 | 20, 65 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(0vecβπ) β (BaseSetβπ) |
67 | | ubth.2 |
. . . . . . . . . . . . . . . . . 18
β’ π =
(normCVβπ) |
68 | 30, 64, 67, 13 | nvnd 29672 |
. . . . . . . . . . . . . . . . 17
β’ ((π β NrmCVec β§ π¦ β (BaseSetβπ)) β (πβπ¦) = (π¦(IndMetβπ)(0vecβπ))) |
69 | 20, 68 | mpan 689 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (BaseSetβπ) β (πβπ¦) = (π¦(IndMetβπ)(0vecβπ))) |
70 | | xmetsym 23716 |
. . . . . . . . . . . . . . . . 17
β’
(((IndMetβπ)
β (βMetβ(BaseSetβπ)) β§ (0vecβπ) β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β ((0vecβπ)(IndMetβπ)π¦) = (π¦(IndMetβπ)(0vecβπ))) |
71 | 32, 66, 70 | mp3an12 1452 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (BaseSetβπ) β
((0vecβπ)(IndMetβπ)π¦) = (π¦(IndMetβπ)(0vecβπ))) |
72 | 69, 71 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (BaseSetβπ) β (πβπ¦) = ((0vecβπ)(IndMetβπ)π¦)) |
73 | 72 | breq1d 5120 |
. . . . . . . . . . . . . 14
β’ (π¦ β (BaseSetβπ) β ((πβπ¦) β€ π β ((0vecβπ)(IndMetβπ)π¦) β€ π)) |
74 | 73 | rabbiia 3414 |
. . . . . . . . . . . . 13
β’ {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π} = {π¦ β (BaseSetβπ) β£ ((0vecβπ)(IndMetβπ)π¦) β€ π} |
75 | 15, 74 | blcld 23877 |
. . . . . . . . . . . 12
β’
(((IndMetβπ)
β (βMetβ(BaseSetβπ)) β§ (0vecβπ) β (BaseSetβπ) β§ π β β*) β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π} β
(Clsdβ(MetOpenβ(IndMetβπ)))) |
76 | 32, 66, 75 | mp3an12 1452 |
. . . . . . . . . . 11
β’ (π β β*
β {π¦ β
(BaseSetβπ) β£
(πβπ¦) β€ π} β
(Clsdβ(MetOpenβ(IndMetβπ)))) |
77 | 63, 76 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π‘ β π) β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π} β
(Clsdβ(MetOpenβ(IndMetβπ)))) |
78 | 58, 60, 77 | rspcdva 3585 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π‘ β π) β (β‘π‘ β {π¦ β (BaseSetβπ) β£ (πβπ¦) β€ π}) β (Clsdβπ½)) |
79 | 56, 78 | eqeltrd 2838 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π‘ β π) β {π§ β π β£ (πβ(π‘βπ§)) β€ π} β (Clsdβπ½)) |
80 | 79 | ralrimiva 3144 |
. . . . . . 7
β’ ((π β§ π β β) β βπ‘ β π {π§ β π β£ (πβ(π‘βπ§)) β€ π} β (Clsdβπ½)) |
81 | | iincld 22406 |
. . . . . . 7
β’ ((π β β
β§
βπ‘ β π {π§ β π β£ (πβ(π‘βπ§)) β€ π} β (Clsdβπ½)) β β© π‘ β π {π§ β π β£ (πβ(π‘βπ§)) β€ π} β (Clsdβπ½)) |
82 | 9, 80, 81 | syl2anr 598 |
. . . . . 6
β’ (((π β§ π β β) β§ π β β
) β β© π‘ β π {π§ β π β£ (πβ(π‘βπ§)) β€ π} β (Clsdβπ½)) |
83 | 8, 82 | eqeltrrd 2839 |
. . . . 5
β’ (((π β§ π β β) β§ π β β
) β {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π} β (Clsdβπ½)) |
84 | 14 | mopntop 23809 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π½ β Top) |
85 | 27, 84 | ax-mp 5 |
. . . . . . 7
β’ π½ β Top |
86 | 29 | toponunii 22281 |
. . . . . . . 8
β’ π = βͺ
π½ |
87 | 86 | topcld 22402 |
. . . . . . 7
β’ (π½ β Top β π β (Clsdβπ½)) |
88 | 85, 87 | ax-mp 5 |
. . . . . 6
β’ π β (Clsdβπ½) |
89 | 88 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β π β (Clsdβπ½)) |
90 | 6, 83, 89 | pm2.61ne 3031 |
. . . 4
β’ ((π β§ π β β) β {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π} β (Clsdβπ½)) |
91 | | ubthlem.9 |
. . . 4
β’ π΄ = (π β β β¦ {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) |
92 | 90, 91 | fmptd 7067 |
. . 3
β’ (π β π΄:ββΆ(Clsdβπ½)) |
93 | 92 | frnd 6681 |
. . . . . 6
β’ (π β ran π΄ β (Clsdβπ½)) |
94 | 86 | cldss2 22397 |
. . . . . 6
β’
(Clsdβπ½)
β π« π |
95 | 93, 94 | sstrdi 3961 |
. . . . 5
β’ (π β ran π΄ β π« π) |
96 | | sspwuni 5065 |
. . . . 5
β’ (ran
π΄ β π« π β βͺ ran π΄ β π) |
97 | 95, 96 | sylib 217 |
. . . 4
β’ (π β βͺ ran π΄ β π) |
98 | | ubthlem.8 |
. . . . . 6
β’ (π β βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π) |
99 | | arch 12417 |
. . . . . . . . . 10
β’ (π β β β
βπ β β
π < π) |
100 | 99 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β β) β βπ β β π < π) |
101 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β π) β§ π β β) β π β β) |
102 | | ltle 11250 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β) β (π < π β π β€ π)) |
103 | 101, 61, 102 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ π β β) β§ π β β) β (π < π β π β€ π)) |
104 | 103 | impr 456 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ π β β) β§ (π β β β§ π < π)) β π β€ π) |
105 | 104 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β π) β§ π β β) β§ (π β β β§ π < π)) β§ π‘ β π) β π β€ π) |
106 | 39 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π‘ β π) β§ π₯ β π) β (π‘βπ₯) β (BaseSetβπ)) |
107 | 106 | an32s 651 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β π) β§ π‘ β π) β (π‘βπ₯) β (BaseSetβπ)) |
108 | 30, 67 | nvcl 29645 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β NrmCVec β§ (π‘βπ₯) β (BaseSetβπ)) β (πβ(π‘βπ₯)) β β) |
109 | 20, 107, 108 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β π) β§ π‘ β π) β (πβ(π‘βπ₯)) β β) |
110 | 109 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ π β β) β§ π‘ β π) β (πβ(π‘βπ₯)) β β) |
111 | 110 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β π) β§ π β β) β§ (π β β β§ π < π)) β§ π‘ β π) β (πβ(π‘βπ₯)) β β) |
112 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β π) β§ π β β) β§ (π β β β§ π < π)) β§ π‘ β π) β π β β) |
113 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β π) β§ π β β) β§ (π β β β§ π < π)) β§ π‘ β π) β π β β) |
114 | 113, 61 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β π) β§ π β β) β§ (π β β β§ π < π)) β§ π‘ β π) β π β β) |
115 | | letr 11256 |
. . . . . . . . . . . . . . 15
β’ (((πβ(π‘βπ₯)) β β β§ π β β β§ π β β) β (((πβ(π‘βπ₯)) β€ π β§ π β€ π) β (πβ(π‘βπ₯)) β€ π)) |
116 | 111, 112,
114, 115 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β π) β§ π β β) β§ (π β β β§ π < π)) β§ π‘ β π) β (((πβ(π‘βπ₯)) β€ π β§ π β€ π) β (πβ(π‘βπ₯)) β€ π)) |
117 | 105, 116 | mpan2d 693 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β π) β§ π β β) β§ (π β β β§ π < π)) β§ π‘ β π) β ((πβ(π‘βπ₯)) β€ π β (πβ(π‘βπ₯)) β€ π)) |
118 | 117 | ralimdva 3165 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ π β β) β§ (π β β β§ π < π)) β (βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ‘ β π (πβ(π‘βπ₯)) β€ π)) |
119 | 118 | expr 458 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π β β) β§ π β β) β (π < π β (βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ‘ β π (πβ(π‘βπ₯)) β€ π))) |
120 | 22 | fvexi 6861 |
. . . . . . . . . . . . . . . . . 18
β’ π β V |
121 | 120 | rabex 5294 |
. . . . . . . . . . . . . . . . 17
β’ {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π} β V |
122 | 91 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π} β V) β (π΄βπ) = {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) |
123 | 121, 122 | mpan2 690 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π΄βπ) = {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) |
124 | 123 | eleq2d 2824 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π₯ β (π΄βπ) β π₯ β {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π})) |
125 | 49 | ralbidv 3175 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π₯ β (βπ‘ β π (πβ(π‘βπ§)) β€ π β βπ‘ β π (πβ(π‘βπ₯)) β€ π)) |
126 | 125 | elrab 3650 |
. . . . . . . . . . . . . . 15
β’ (π₯ β {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π} β (π₯ β π β§ βπ‘ β π (πβ(π‘βπ₯)) β€ π)) |
127 | 124, 126 | bitrdi 287 |
. . . . . . . . . . . . . 14
β’ (π β β β (π₯ β (π΄βπ) β (π₯ β π β§ βπ‘ β π (πβ(π‘βπ₯)) β€ π))) |
128 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π) β π₯ β π) |
129 | 128 | biantrurd 534 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π) β (βπ‘ β π (πβ(π‘βπ₯)) β€ π β (π₯ β π β§ βπ‘ β π (πβ(π‘βπ₯)) β€ π))) |
130 | 129 | bicomd 222 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β ((π₯ β π β§ βπ‘ β π (πβ(π‘βπ₯)) β€ π) β βπ‘ β π (πβ(π‘βπ₯)) β€ π)) |
131 | 127, 130 | sylan9bbr 512 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ π β β) β (π₯ β (π΄βπ) β βπ‘ β π (πβ(π‘βπ₯)) β€ π)) |
132 | 92 | ffnd 6674 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ Fn β) |
133 | 132 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β π΄ Fn β) |
134 | | fnfvelrn 7036 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ Fn β β§ π β β) β (π΄βπ) β ran π΄) |
135 | | elssuni 4903 |
. . . . . . . . . . . . . . . 16
β’ ((π΄βπ) β ran π΄ β (π΄βπ) β βͺ ran
π΄) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π΄ Fn β β§ π β β) β (π΄βπ) β βͺ ran
π΄) |
137 | 136 | sseld 3948 |
. . . . . . . . . . . . . 14
β’ ((π΄ Fn β β§ π β β) β (π₯ β (π΄βπ) β π₯ β βͺ ran
π΄)) |
138 | 133, 137 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ π β β) β (π₯ β (π΄βπ) β π₯ β βͺ ran
π΄)) |
139 | 131, 138 | sylbird 260 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π β β) β (βπ‘ β π (πβ(π‘βπ₯)) β€ π β π₯ β βͺ ran
π΄)) |
140 | 139 | adantlr 714 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π β β) β§ π β β) β (βπ‘ β π (πβ(π‘βπ₯)) β€ π β π₯ β βͺ ran
π΄)) |
141 | 119, 140 | syl6d 75 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ π β β) β§ π β β) β (π < π β (βπ‘ β π (πβ(π‘βπ₯)) β€ π β π₯ β βͺ ran
π΄))) |
142 | 141 | rexlimdva 3153 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β β) β (βπ β β π < π β (βπ‘ β π (πβ(π‘βπ₯)) β€ π β π₯ β βͺ ran
π΄))) |
143 | 100, 142 | mpd 15 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β β) β (βπ‘ β π (πβ(π‘βπ₯)) β€ π β π₯ β βͺ ran
π΄)) |
144 | 143 | rexlimdva 3153 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β π₯ β βͺ ran
π΄)) |
145 | 144 | ralimdva 3165 |
. . . . . 6
β’ (π β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ₯ β π π₯ β βͺ ran
π΄)) |
146 | 98, 145 | mpd 15 |
. . . . 5
β’ (π β βπ₯ β π π₯ β βͺ ran
π΄) |
147 | | dfss3 3937 |
. . . . 5
β’ (π β βͺ ran π΄ β βπ₯ β π π₯ β βͺ ran
π΄) |
148 | 146, 147 | sylibr 233 |
. . . 4
β’ (π β π β βͺ ran
π΄) |
149 | 97, 148 | eqssd 3966 |
. . 3
β’ (π β βͺ ran π΄ = π) |
150 | | eqid 2737 |
. . . . . 6
β’
(0vecβπ) = (0vecβπ) |
151 | 22, 150 | nvzcl 29618 |
. . . . 5
β’ (π β NrmCVec β
(0vecβπ)
β π) |
152 | | ne0i 4299 |
. . . . 5
β’
((0vecβπ) β π β π β β
) |
153 | 19, 151, 152 | mp2b 10 |
. . . 4
β’ π β β
|
154 | 14 | bcth2 24710 |
. . . 4
β’ (((π· β (CMetβπ) β§ π β β
) β§ (π΄:ββΆ(Clsdβπ½) β§ βͺ ran π΄ = π)) β βπ β β ((intβπ½)β(π΄βπ)) β β
) |
155 | 24, 153, 154 | mpanl12 701 |
. . 3
β’ ((π΄:ββΆ(Clsdβπ½) β§ βͺ ran π΄ = π) β βπ β β ((intβπ½)β(π΄βπ)) β β
) |
156 | 92, 149, 155 | syl2anc 585 |
. 2
β’ (π β βπ β β ((intβπ½)β(π΄βπ)) β β
) |
157 | | ffvelcdm 7037 |
. . . . . . . . . . 11
β’ ((π΄:ββΆ(Clsdβπ½) β§ π β β) β (π΄βπ) β (Clsdβπ½)) |
158 | 94, 157 | sselid 3947 |
. . . . . . . . . 10
β’ ((π΄:ββΆ(Clsdβπ½) β§ π β β) β (π΄βπ) β π« π) |
159 | 158 | elpwid 4574 |
. . . . . . . . 9
β’ ((π΄:ββΆ(Clsdβπ½) β§ π β β) β (π΄βπ) β π) |
160 | 92, 159 | sylan 581 |
. . . . . . . 8
β’ ((π β§ π β β) β (π΄βπ) β π) |
161 | 86 | ntrss3 22427 |
. . . . . . . 8
β’ ((π½ β Top β§ (π΄βπ) β π) β ((intβπ½)β(π΄βπ)) β π) |
162 | 85, 160, 161 | sylancr 588 |
. . . . . . 7
β’ ((π β§ π β β) β ((intβπ½)β(π΄βπ)) β π) |
163 | 162 | sseld 3948 |
. . . . . 6
β’ ((π β§ π β β) β (π¦ β ((intβπ½)β(π΄βπ)) β π¦ β π)) |
164 | 86 | ntropn 22416 |
. . . . . . . . . 10
β’ ((π½ β Top β§ (π΄βπ) β π) β ((intβπ½)β(π΄βπ)) β π½) |
165 | 85, 160, 164 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((intβπ½)β(π΄βπ)) β π½) |
166 | 14 | mopni2 23865 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ ((intβπ½)β(π΄βπ)) β π½ β§ π¦ β ((intβπ½)β(π΄βπ))) β βπ₯ β β+ (π¦(ballβπ·)π₯) β ((intβπ½)β(π΄βπ))) |
167 | 27, 166 | mp3an1 1449 |
. . . . . . . . 9
β’
((((intβπ½)β(π΄βπ)) β π½ β§ π¦ β ((intβπ½)β(π΄βπ))) β βπ₯ β β+ (π¦(ballβπ·)π₯) β ((intβπ½)β(π΄βπ))) |
168 | 165, 167 | sylan 581 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β ((intβπ½)β(π΄βπ))) β βπ₯ β β+ (π¦(ballβπ·)π₯) β ((intβπ½)β(π΄βπ))) |
169 | | elssuni 4903 |
. . . . . . . . . . . 12
β’
(((intβπ½)β(π΄βπ)) β π½ β ((intβπ½)β(π΄βπ)) β βͺ π½) |
170 | 169, 86 | sseqtrrdi 4000 |
. . . . . . . . . . 11
β’
(((intβπ½)β(π΄βπ)) β π½ β ((intβπ½)β(π΄βπ)) β π) |
171 | 165, 170 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((intβπ½)β(π΄βπ)) β π) |
172 | 171 | sselda 3949 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π¦ β ((intβπ½)β(π΄βπ))) β π¦ β π) |
173 | 86 | ntrss2 22424 |
. . . . . . . . . . . . . 14
β’ ((π½ β Top β§ (π΄βπ) β π) β ((intβπ½)β(π΄βπ)) β (π΄βπ)) |
174 | 85, 160, 173 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((intβπ½)β(π΄βπ)) β (π΄βπ)) |
175 | | sstr2 3956 |
. . . . . . . . . . . . 13
β’ ((π¦(ballβπ·)π₯) β ((intβπ½)β(π΄βπ)) β (((intβπ½)β(π΄βπ)) β (π΄βπ) β (π¦(ballβπ·)π₯) β (π΄βπ))) |
176 | 174, 175 | syl5com 31 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π¦(ballβπ·)π₯) β ((intβπ½)β(π΄βπ)) β (π¦(ballβπ·)π₯) β (π΄βπ))) |
177 | 176 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ π¦ β π) β§ π₯ β β+) β ((π¦(ballβπ·)π₯) β ((intβπ½)β(π΄βπ)) β (π¦(ballβπ·)π₯) β (π΄βπ))) |
178 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π¦ β π) β π¦ β π) |
179 | 178, 27 | jctil 521 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π¦ β π) β (π· β (βMetβπ) β§ π¦ β π)) |
180 | | rphalfcl 12949 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β (π₯ / 2) β
β+) |
181 | 180 | rpxrd 12965 |
. . . . . . . . . . . . . 14
β’ (π₯ β β+
β (π₯ / 2) β
β*) |
182 | | rpxr 12931 |
. . . . . . . . . . . . . 14
β’ (π₯ β β+
β π₯ β
β*) |
183 | | rphalflt 12951 |
. . . . . . . . . . . . . 14
β’ (π₯ β β+
β (π₯ / 2) < π₯) |
184 | 181, 182,
183 | 3jca 1129 |
. . . . . . . . . . . . 13
β’ (π₯ β β+
β ((π₯ / 2) β
β* β§ π₯
β β* β§ (π₯ / 2) < π₯)) |
185 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ {π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} = {π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} |
186 | 14, 185 | blsscls2 23876 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π¦ β π) β§ ((π₯ / 2) β β* β§ π₯ β β*
β§ (π₯ / 2) < π₯)) β {π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} β (π¦(ballβπ·)π₯)) |
187 | 179, 184,
186 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ π¦ β π) β§ π₯ β β+) β {π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} β (π¦(ballβπ·)π₯)) |
188 | | sstr2 3956 |
. . . . . . . . . . . 12
β’ ({π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} β (π¦(ballβπ·)π₯) β ((π¦(ballβπ·)π₯) β (π΄βπ) β {π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} β (π΄βπ))) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ π¦ β π) β§ π₯ β β+) β ((π¦(ballβπ·)π₯) β (π΄βπ) β {π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} β (π΄βπ))) |
190 | 180 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ π¦ β π) β§ π₯ β β+) β (π₯ / 2) β
β+) |
191 | | breq2 5114 |
. . . . . . . . . . . . . . . 16
β’ (π = (π₯ / 2) β ((π¦π·π§) β€ π β (π¦π·π§) β€ (π₯ / 2))) |
192 | 191 | rabbidv 3418 |
. . . . . . . . . . . . . . 15
β’ (π = (π₯ / 2) β {π§ β π β£ (π¦π·π§) β€ π} = {π§ β π β£ (π¦π·π§) β€ (π₯ / 2)}) |
193 | 192 | sseq1d 3980 |
. . . . . . . . . . . . . 14
β’ (π = (π₯ / 2) β ({π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ) β {π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} β (π΄βπ))) |
194 | 193 | rspcev 3584 |
. . . . . . . . . . . . 13
β’ (((π₯ / 2) β β+
β§ {π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} β (π΄βπ)) β βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ)) |
195 | 194 | ex 414 |
. . . . . . . . . . . 12
β’ ((π₯ / 2) β β+
β ({π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} β (π΄βπ) β βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ))) |
196 | 190, 195 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ π¦ β π) β§ π₯ β β+) β ({π§ β π β£ (π¦π·π§) β€ (π₯ / 2)} β (π΄βπ) β βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ))) |
197 | 177, 189,
196 | 3syld 60 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ π¦ β π) β§ π₯ β β+) β ((π¦(ballβπ·)π₯) β ((intβπ½)β(π΄βπ)) β βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ))) |
198 | 197 | rexlimdva 3153 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π¦ β π) β (βπ₯ β β+ (π¦(ballβπ·)π₯) β ((intβπ½)β(π΄βπ)) β βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ))) |
199 | 172, 198 | syldan 592 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β ((intβπ½)β(π΄βπ))) β (βπ₯ β β+ (π¦(ballβπ·)π₯) β ((intβπ½)β(π΄βπ)) β βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ))) |
200 | 168, 199 | mpd 15 |
. . . . . . 7
β’ (((π β§ π β β) β§ π¦ β ((intβπ½)β(π΄βπ))) β βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ)) |
201 | 200 | ex 414 |
. . . . . 6
β’ ((π β§ π β β) β (π¦ β ((intβπ½)β(π΄βπ)) β βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ))) |
202 | 163, 201 | jcad 514 |
. . . . 5
β’ ((π β§ π β β) β (π¦ β ((intβπ½)β(π΄βπ)) β (π¦ β π β§ βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ)))) |
203 | 202 | eximdv 1921 |
. . . 4
β’ ((π β§ π β β) β (βπ¦ π¦ β ((intβπ½)β(π΄βπ)) β βπ¦(π¦ β π β§ βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ)))) |
204 | | n0 4311 |
. . . 4
β’
(((intβπ½)β(π΄βπ)) β β
β βπ¦ π¦ β ((intβπ½)β(π΄βπ))) |
205 | | df-rex 3075 |
. . . 4
β’
(βπ¦ β
π βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ) β βπ¦(π¦ β π β§ βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ))) |
206 | 203, 204,
205 | 3imtr4g 296 |
. . 3
β’ ((π β§ π β β) β (((intβπ½)β(π΄βπ)) β β
β βπ¦ β π βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ))) |
207 | 206 | reximdva 3166 |
. 2
β’ (π β (βπ β β ((intβπ½)β(π΄βπ)) β β
β βπ β β βπ¦ β π βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ))) |
208 | 156, 207 | mpd 15 |
1
β’ (π β βπ β β βπ¦ β π βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ)) |