Step | Hyp | Ref
| Expression |
1 | | df-rab 3433 |
. 2
β’ {π β ( β
βm β) β£ βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯} = {π β£ (π β ( β βm β)
β§ βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)} |
2 | | df-hcau 30221 |
. 2
β’ Cauchy =
{π β ( β
βm β) β£ βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯} |
3 | | elin 3964 |
. . . 4
β’ (π β ((Cauβπ·) β© ( β
βm β)) β (π β (Cauβπ·) β§ π β ( β βm
β))) |
4 | | ancom 461 |
. . . 4
β’ ((π β (Cauβπ·) β§ π β ( β βm
β)) β (π β
( β βm β) β§ π β (Cauβπ·))) |
5 | | h2hc.3 |
. . . . . . . 8
β’ β
= (BaseSetβπ) |
6 | 5 | hlex 30146 |
. . . . . . 7
β’ β
β V |
7 | | nnex 12217 |
. . . . . . 7
β’ β
β V |
8 | 6, 7 | elmap 8864 |
. . . . . 6
β’ (π β ( β
βm β) β π:ββΆ β) |
9 | | nnuz 12864 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
10 | | h2hc.2 |
. . . . . . . . 9
β’ π β NrmCVec |
11 | | h2hc.4 |
. . . . . . . . . 10
β’ π· = (IndMetβπ) |
12 | 5, 11 | imsxmet 29940 |
. . . . . . . . 9
β’ (π β NrmCVec β π· β (βMetβ
β)) |
13 | 10, 12 | mp1i 13 |
. . . . . . . 8
β’ (π:ββΆ β β
π· β (βMetβ
β)) |
14 | | 1zzd 12592 |
. . . . . . . 8
β’ (π:ββΆ β β
1 β β€) |
15 | | eqidd 2733 |
. . . . . . . 8
β’ ((π:ββΆ β β§
π β β) β
(πβπ) = (πβπ)) |
16 | | eqidd 2733 |
. . . . . . . 8
β’ ((π:ββΆ β β§
π β β) β
(πβπ) = (πβπ)) |
17 | | id 22 |
. . . . . . . 8
β’ (π:ββΆ β β
π:ββΆ
β) |
18 | 9, 13, 14, 15, 16, 17 | iscauf 24796 |
. . . . . . 7
β’ (π:ββΆ β β
(π β (Cauβπ·) β βπ₯ β β+
βπ β β
βπ β
(β€β₯βπ)((πβπ)π·(πβπ)) < π₯)) |
19 | | ffvelcdm 7083 |
. . . . . . . . . . . . 13
β’ ((π:ββΆ β β§
π β β) β
(πβπ) β β) |
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π:ββΆ β β§
π β β) β§
π β
(β€β₯βπ)) β (πβπ) β β) |
21 | | eluznn 12901 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
22 | | ffvelcdm 7083 |
. . . . . . . . . . . . . 14
β’ ((π:ββΆ β β§
π β β) β
(πβπ) β β) |
23 | 21, 22 | sylan2 593 |
. . . . . . . . . . . . 13
β’ ((π:ββΆ β β§
(π β β β§
π β
(β€β₯βπ))) β (πβπ) β β) |
24 | 23 | anassrs 468 |
. . . . . . . . . . . 12
β’ (((π:ββΆ β β§
π β β) β§
π β
(β€β₯βπ)) β (πβπ) β β) |
25 | | h2hc.1 |
. . . . . . . . . . . . 13
β’ π = β¨β¨
+β , Β·β β©,
normββ© |
26 | 25, 10, 5, 11 | h2hmetdval 30226 |
. . . . . . . . . . . 12
β’ (((πβπ) β β β§ (πβπ) β β) β ((πβπ)π·(πβπ)) = (normββ((πβπ) ββ (πβπ)))) |
27 | 20, 24, 26 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π:ββΆ β β§
π β β) β§
π β
(β€β₯βπ)) β ((πβπ)π·(πβπ)) = (normββ((πβπ) ββ (πβπ)))) |
28 | 27 | breq1d 5158 |
. . . . . . . . . 10
β’ (((π:ββΆ β β§
π β β) β§
π β
(β€β₯βπ)) β (((πβπ)π·(πβπ)) < π₯ β
(normββ((πβπ) ββ (πβπ))) < π₯)) |
29 | 28 | ralbidva 3175 |
. . . . . . . . 9
β’ ((π:ββΆ β β§
π β β) β
(βπ β
(β€β₯βπ)((πβπ)π·(πβπ)) < π₯ β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
30 | 29 | rexbidva 3176 |
. . . . . . . 8
β’ (π:ββΆ β β
(βπ β β
βπ β
(β€β₯βπ)((πβπ)π·(πβπ)) < π₯ β βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
31 | 30 | ralbidv 3177 |
. . . . . . 7
β’ (π:ββΆ β β
(βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)((πβπ)π·(πβπ)) < π₯ β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
32 | 18, 31 | bitrd 278 |
. . . . . 6
β’ (π:ββΆ β β
(π β (Cauβπ·) β βπ₯ β β+
βπ β β
βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
33 | 8, 32 | sylbi 216 |
. . . . 5
β’ (π β ( β
βm β) β (π β (Cauβπ·) β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
34 | 33 | pm5.32i 575 |
. . . 4
β’ ((π β ( β
βm β) β§ π β (Cauβπ·)) β (π β ( β βm β)
β§ βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
35 | 3, 4, 34 | 3bitri 296 |
. . 3
β’ (π β ((Cauβπ·) β© ( β
βm β)) β (π β ( β βm β)
β§ βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)) |
36 | 35 | eqabi 2869 |
. 2
β’
((Cauβπ·) β©
( β βm β)) = {π β£ (π β ( β βm β)
β§ βπ₯ β
β+ βπ β β βπ β (β€β₯βπ)(normββ((πβπ) ββ (πβπ))) < π₯)} |
37 | 1, 2, 36 | 3eqtr4i 2770 |
1
β’ Cauchy =
((Cauβπ·) β© (
β βm β)) |