Step | Hyp | Ref
| Expression |
1 | | simplll 774 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β π΄ β β) |
2 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β π₯ β π΄) |
3 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β π€ β π΄) |
4 | | cncfmet.1 |
. . . . . . . . . . . . . . . 16
β’ πΆ = ((abs β β )
βΎ (π΄ Γ π΄)) |
5 | 4 | oveqi 7374 |
. . . . . . . . . . . . . . 15
β’ (π₯πΆπ€) = (π₯((abs β β ) βΎ (π΄ Γ π΄))π€) |
6 | | ovres 7524 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π΄ β§ π€ β π΄) β (π₯((abs β β ) βΎ (π΄ Γ π΄))π€) = (π₯(abs β β )π€)) |
7 | 5, 6 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π΄ β§ π€ β π΄) β (π₯πΆπ€) = (π₯(abs β β )π€)) |
8 | 7 | ad2ant2l 745 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ π₯ β π΄) β§ (π΄ β β β§ π€ β π΄)) β (π₯πΆπ€) = (π₯(abs β β )π€)) |
9 | | ssel2 3943 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π₯ β π΄) β π₯ β β) |
10 | | ssel2 3943 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π€ β π΄) β π€ β β) |
11 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (abs
β β ) = (abs β β ) |
12 | 11 | cnmetdval 24157 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π€ β β) β (π₯(abs β β )π€) = (absβ(π₯ β π€))) |
13 | 9, 10, 12 | syl2an 597 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ π₯ β π΄) β§ (π΄ β β β§ π€ β π΄)) β (π₯(abs β β )π€) = (absβ(π₯ β π€))) |
14 | 8, 13 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ π₯ β π΄) β§ (π΄ β β β§ π€ β π΄)) β (π₯πΆπ€) = (absβ(π₯ β π€))) |
15 | 1, 2, 1, 3, 14 | syl22anc 838 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β (π₯πΆπ€) = (absβ(π₯ β π€))) |
16 | 15 | breq1d 5119 |
. . . . . . . . . 10
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β ((π₯πΆπ€) < π§ β (absβ(π₯ β π€)) < π§)) |
17 | | ffvelcdm 7036 |
. . . . . . . . . . . . . 14
β’ ((π:π΄βΆπ΅ β§ π₯ β π΄) β (πβπ₯) β π΅) |
18 | 17 | ad2ant2lr 747 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β (πβπ₯) β π΅) |
19 | | ffvelcdm 7036 |
. . . . . . . . . . . . . 14
β’ ((π:π΄βΆπ΅ β§ π€ β π΄) β (πβπ€) β π΅) |
20 | 19 | ad2ant2l 745 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β (πβπ€) β π΅) |
21 | | cncfmet.2 |
. . . . . . . . . . . . . . 15
β’ π· = ((abs β β )
βΎ (π΅ Γ π΅)) |
22 | 21 | oveqi 7374 |
. . . . . . . . . . . . . 14
β’ ((πβπ₯)π·(πβπ€)) = ((πβπ₯)((abs β β ) βΎ (π΅ Γ π΅))(πβπ€)) |
23 | | ovres 7524 |
. . . . . . . . . . . . . 14
β’ (((πβπ₯) β π΅ β§ (πβπ€) β π΅) β ((πβπ₯)((abs β β ) βΎ (π΅ Γ π΅))(πβπ€)) = ((πβπ₯)(abs β β )(πβπ€))) |
24 | 22, 23 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (((πβπ₯) β π΅ β§ (πβπ€) β π΅) β ((πβπ₯)π·(πβπ€)) = ((πβπ₯)(abs β β )(πβπ€))) |
25 | 18, 20, 24 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β ((πβπ₯)π·(πβπ€)) = ((πβπ₯)(abs β β )(πβπ€))) |
26 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β π΅ β β) |
27 | 26, 18 | sseldd 3949 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β (πβπ₯) β β) |
28 | 26, 20 | sseldd 3949 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β (πβπ€) β β) |
29 | 11 | cnmetdval 24157 |
. . . . . . . . . . . . 13
β’ (((πβπ₯) β β β§ (πβπ€) β β) β ((πβπ₯)(abs β β )(πβπ€)) = (absβ((πβπ₯) β (πβπ€)))) |
30 | 27, 28, 29 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β ((πβπ₯)(abs β β )(πβπ€)) = (absβ((πβπ₯) β (πβπ€)))) |
31 | 25, 30 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β ((πβπ₯)π·(πβπ€)) = (absβ((πβπ₯) β (πβπ€)))) |
32 | 31 | breq1d 5119 |
. . . . . . . . . 10
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β (((πβπ₯)π·(πβπ€)) < π¦ β (absβ((πβπ₯) β (πβπ€))) < π¦)) |
33 | 16, 32 | imbi12d 345 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ (π₯ β π΄ β§ π€ β π΄)) β (((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦))) |
34 | 33 | anassrs 469 |
. . . . . . . 8
β’
(((((π΄ β
β β§ π΅ β
β) β§ π:π΄βΆπ΅) β§ π₯ β π΄) β§ π€ β π΄) β (((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦))) |
35 | 34 | ralbidva 3169 |
. . . . . . 7
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ π₯ β π΄) β (βπ€ β π΄ ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦))) |
36 | 35 | rexbidv 3172 |
. . . . . 6
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ π₯ β π΄) β (βπ§ β β+ βπ€ β π΄ ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ§ β β+ βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦))) |
37 | 36 | ralbidv 3171 |
. . . . 5
β’ ((((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β§ π₯ β π΄) β (βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦))) |
38 | 37 | ralbidva 3169 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§ π:π΄βΆπ΅) β (βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦))) |
39 | 38 | pm5.32da 580 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β ((π:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)) β (π:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦)))) |
40 | | cnxmet 24159 |
. . . . . 6
β’ (abs
β β ) β (βMetββ) |
41 | | xmetres2 23737 |
. . . . . 6
β’ (((abs
β β ) β (βMetββ) β§ π΄ β β) β ((abs β
β ) βΎ (π΄
Γ π΄)) β
(βMetβπ΄)) |
42 | 40, 41 | mpan 689 |
. . . . 5
β’ (π΄ β β β ((abs
β β ) βΎ (π΄ Γ π΄)) β (βMetβπ΄)) |
43 | 4, 42 | eqeltrid 2838 |
. . . 4
β’ (π΄ β β β πΆ β (βMetβπ΄)) |
44 | | xmetres2 23737 |
. . . . . 6
β’ (((abs
β β ) β (βMetββ) β§ π΅ β β) β ((abs β
β ) βΎ (π΅
Γ π΅)) β
(βMetβπ΅)) |
45 | 40, 44 | mpan 689 |
. . . . 5
β’ (π΅ β β β ((abs
β β ) βΎ (π΅ Γ π΅)) β (βMetβπ΅)) |
46 | 21, 45 | eqeltrid 2838 |
. . . 4
β’ (π΅ β β β π· β (βMetβπ΅)) |
47 | | cncfmet.3 |
. . . . 5
β’ π½ = (MetOpenβπΆ) |
48 | | cncfmet.4 |
. . . . 5
β’ πΎ = (MetOpenβπ·) |
49 | 47, 48 | metcn 23922 |
. . . 4
β’ ((πΆ β (βMetβπ΄) β§ π· β (βMetβπ΅)) β (π β (π½ Cn πΎ) β (π:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)))) |
50 | 43, 46, 49 | syl2an 597 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β (π β (π½ Cn πΎ) β (π:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)))) |
51 | | elcncf 24275 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β (π β (π΄βcnβπ΅) β (π:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦)))) |
52 | 39, 50, 51 | 3bitr4rd 312 |
. 2
β’ ((π΄ β β β§ π΅ β β) β (π β (π΄βcnβπ΅) β π β (π½ Cn πΎ))) |
53 | 52 | eqrdv 2731 |
1
β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = (π½ Cn πΎ)) |