Step | Hyp | Ref
| Expression |
1 | | df-rab 3407 |
. 2
β’ {π β ( β
βm β) β£ βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯} = {π β£ (π β ( β βm β)
β§ βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)} |
2 | | df-hcau 29964 |
. 2
β’ Cauchy =
{π β ( β
βm β) β£ βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯} |
3 | | elin 3930 |
. . . 4
β’ (π β ((Cauβπ·) β© ( β
βm β)) β (π β (Cauβπ·) β§ π β ( β βm
β))) |
4 | | ancom 462 |
. . . 4
β’ ((π β (Cauβπ·) β§ π β ( β βm
β)) β (π β
( β βm β) β§ π β (Cauβπ·))) |
5 | | h2hc.3 |
. . . . . . . 8
β’ β
= (BaseSetβπ) |
6 | 5 | hlex 29889 |
. . . . . . 7
β’ β
β V |
7 | | nnex 12167 |
. . . . . . 7
β’ β
β V |
8 | 6, 7 | elmap 8815 |
. . . . . 6
β’ (π β ( β
βm β) β π:ββΆ β) |
9 | | nnuz 12814 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
10 | | h2hc.2 |
. . . . . . . . 9
β’ π β NrmCVec |
11 | | h2hc.4 |
. . . . . . . . . 10
β’ π· = (IndMetβπ) |
12 | 5, 11 | imsxmet 29683 |
. . . . . . . . 9
β’ (π β NrmCVec β π· β (βMetβ
β)) |
13 | 10, 12 | mp1i 13 |
. . . . . . . 8
β’ (π:ββΆ β β
π· β (βMetβ
β)) |
14 | | 1zzd 12542 |
. . . . . . . 8
β’ (π:ββΆ β β
1 β β€) |
15 | | eqidd 2734 |
. . . . . . . 8
β’ ((π:ββΆ β β§
π β β) β
(πβπ) = (πβπ)) |
16 | | eqidd 2734 |
. . . . . . . 8
β’ ((π:ββΆ β β§
π β β) β
(πβπ) = (πβπ)) |
17 | | id 22 |
. . . . . . . 8
β’ (π:ββΆ β β
π:ββΆ
β) |
18 | 9, 13, 14, 15, 16, 17 | iscauf 24667 |
. . . . . . 7
β’ (π:ββΆ β β
(π β (Cauβπ·) β βπ₯ β β+
βπ β β
βπ β
(β€β₯βπ)((πβπ)π·(πβπ)) < π₯)) |
19 | | ffvelcdm 7036 |
. . . . . . . . . . . . 13
β’ ((π:ββΆ β β§
π β β) β
(πβπ) β β) |
20 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π:ββΆ β β§
π β β) β§
π β
(β€β₯βπ)) β (πβπ) β β) |
21 | | eluznn 12851 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
22 | | ffvelcdm 7036 |
. . . . . . . . . . . . . 14
β’ ((π:ββΆ β β§
π β β) β
(πβπ) β β) |
23 | 21, 22 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π:ββΆ β β§
(π β β β§
π β
(β€β₯βπ))) β (πβπ) β β) |
24 | 23 | anassrs 469 |
. . . . . . . . . . . 12
β’ (((π:ββΆ β β§
π β β) β§
π β
(β€β₯βπ)) β (πβπ) β β) |
25 | | h2hc.1 |
. . . . . . . . . . . . 13
β’ π = β¨β¨
+β , Β·β β©,
normββ© |
26 | 25, 10, 5, 11 | h2hmetdval 29969 |
. . . . . . . . . . . 12
β’ (((πβπ) β β β§ (πβπ) β β) β ((πβπ)π·(πβπ)) = (normββ((πβπ) ββ (πβπ)))) |
27 | 20, 24, 26 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π:ββΆ β β§
π β β) β§
π β
(β€β₯βπ)) β ((πβπ)π·(πβπ)) = (normββ((πβπ) ββ (πβπ)))) |
28 | 27 | breq1d 5119 |
. . . . . . . . . 10
β’ (((π:ββΆ β β§
π β β) β§
π β
(β€β₯βπ)) β (((πβπ)π·(πβπ)) < π₯ β
(normββ((πβπ) ββ (πβπ))) < π₯)) |
29 | 28 | ralbidva 3169 |
. . . . . . . . 9
β’ ((π:ββΆ β β§
π β β) β
(βπ β
(β€β₯βπ)((πβπ)π·(πβπ)) < π₯ β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
30 | 29 | rexbidva 3170 |
. . . . . . . 8
β’ (π:ββΆ β β
(βπ β β
βπ β
(β€β₯βπ)((πβπ)π·(πβπ)) < π₯ β βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
31 | 30 | ralbidv 3171 |
. . . . . . 7
β’ (π:ββΆ β β
(βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)((πβπ)π·(πβπ)) < π₯ β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
32 | 18, 31 | bitrd 279 |
. . . . . 6
β’ (π:ββΆ β β
(π β (Cauβπ·) β βπ₯ β β+
βπ β β
βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
33 | 8, 32 | sylbi 216 |
. . . . 5
β’ (π β ( β
βm β) β (π β (Cauβπ·) β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
34 | 33 | pm5.32i 576 |
. . . 4
β’ ((π β ( β
βm β) β§ π β (Cauβπ·)) β (π β ( β βm β)
β§ βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
35 | 3, 4, 34 | 3bitri 297 |
. . 3
β’ (π β ((Cauβπ·) β© ( β
βm β)) β (π β ( β βm β)
β§ βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
36 | 35 | abbi2i 2870 |
. 2
β’
((Cauβπ·) β©
( β βm β)) = {π β£ (π β ( β βm β)
β§ βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)} |
37 | 1, 2, 36 | 3eqtr4i 2771 |
1
β’ Cauchy =
((Cauβπ·) β© (
β βm β)) |