Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β π¦ β πΌ) |
2 | | prdsdsf.r |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β πΌ) β π
β π) |
3 | 2 | elexd 3464 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β πΌ) β π
β V) |
4 | 3 | ralrimiva 3142 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ₯ β πΌ π
β V) |
5 | 4 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ π
β V) |
6 | | nfcsb1v 3879 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯β¦π¦ / π₯β¦π
|
7 | 6 | nfel1 2922 |
. . . . . . . . . . . . . . . 16
β’
β²π₯β¦π¦ / π₯β¦π
β V |
8 | | csbeq1a 3868 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β π
= β¦π¦ / π₯β¦π
) |
9 | 8 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (π
β V β β¦π¦ / π₯β¦π
β V)) |
10 | 7, 9 | rspc 3568 |
. . . . . . . . . . . . . . 15
β’ (π¦ β πΌ β (βπ₯ β πΌ π
β V β β¦π¦ / π₯β¦π
β V)) |
11 | 5, 10 | mpan9 508 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β β¦π¦ / π₯β¦π
β V) |
12 | | eqid 2738 |
. . . . . . . . . . . . . . 15
β’ (π₯ β πΌ β¦ π
) = (π₯ β πΌ β¦ π
) |
13 | 12 | fvmpts 6947 |
. . . . . . . . . . . . . 14
β’ ((π¦ β πΌ β§ β¦π¦ / π₯β¦π
β V) β ((π₯ β πΌ β¦ π
)βπ¦) = β¦π¦ / π₯β¦π
) |
14 | 1, 11, 13 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β ((π₯ β πΌ β¦ π
)βπ¦) = β¦π¦ / π₯β¦π
) |
15 | 14 | fveq2d 6842 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β (distβ((π₯ β πΌ β¦ π
)βπ¦)) = (distββ¦π¦ / π₯β¦π
)) |
16 | 15 | oveqd 7367 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦)) = ((πβπ¦)(distββ¦π¦ / π₯β¦π
)(πβπ¦))) |
17 | | prdsdsf.y |
. . . . . . . . . . . . . 14
β’ π = (πXs(π₯ β πΌ β¦ π
)) |
18 | | prdsdsf.b |
. . . . . . . . . . . . . 14
β’ π΅ = (Baseβπ) |
19 | | prdsdsf.s |
. . . . . . . . . . . . . . 15
β’ (π β π β π) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π) |
21 | | prdsdsf.i |
. . . . . . . . . . . . . . 15
β’ (π β πΌ β π) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅)) β πΌ β π) |
23 | | prdsdsf.v |
. . . . . . . . . . . . . 14
β’ π = (Baseβπ
) |
24 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
25 | 17, 18, 20, 22, 5, 23, 24 | prdsbascl 17300 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ (πβπ₯) β π) |
26 | | nfcsb1v 3879 |
. . . . . . . . . . . . . . 15
β’
β²π₯β¦π¦ / π₯β¦π |
27 | 26 | nfel2 2924 |
. . . . . . . . . . . . . 14
β’
β²π₯(πβπ¦) β β¦π¦ / π₯β¦π |
28 | | fveq2 6838 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β (πβπ₯) = (πβπ¦)) |
29 | | csbeq1a 3868 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β π = β¦π¦ / π₯β¦π) |
30 | 28, 29 | eleq12d 2833 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β ((πβπ₯) β π β (πβπ¦) β β¦π¦ / π₯β¦π)) |
31 | 27, 30 | rspc 3568 |
. . . . . . . . . . . . 13
β’ (π¦ β πΌ β (βπ₯ β πΌ (πβπ₯) β π β (πβπ¦) β β¦π¦ / π₯β¦π)) |
32 | 25, 31 | mpan9 508 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β (πβπ¦) β β¦π¦ / π₯β¦π) |
33 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β π΅)) β π β π΅) |
34 | 17, 18, 20, 22, 5, 23, 33 | prdsbascl 17300 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ (πβπ₯) β π) |
35 | 26 | nfel2 2924 |
. . . . . . . . . . . . . 14
β’
β²π₯(πβπ¦) β β¦π¦ / π₯β¦π |
36 | | fveq2 6838 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β (πβπ₯) = (πβπ¦)) |
37 | 36, 29 | eleq12d 2833 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β ((πβπ₯) β π β (πβπ¦) β β¦π¦ / π₯β¦π)) |
38 | 35, 37 | rspc 3568 |
. . . . . . . . . . . . 13
β’ (π¦ β πΌ β (βπ₯ β πΌ (πβπ₯) β π β (πβπ¦) β β¦π¦ / π₯β¦π)) |
39 | 34, 38 | mpan9 508 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β (πβπ¦) β β¦π¦ / π₯β¦π) |
40 | 32, 39 | ovresd 7514 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β ((πβπ¦)((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π))(πβπ¦)) = ((πβπ¦)(distββ¦π¦ / π₯β¦π
)(πβπ¦))) |
41 | 16, 40 | eqtr4d 2781 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦)) = ((πβπ¦)((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π))(πβπ¦))) |
42 | | prdsdsf.m |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
43 | 42 | ralrimiva 3142 |
. . . . . . . . . . . . 13
β’ (π β βπ₯ β πΌ πΈ β (βMetβπ)) |
44 | 43 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π΅ β§ π β π΅)) β βπ₯ β πΌ πΈ β (βMetβπ)) |
45 | | nfcv 2906 |
. . . . . . . . . . . . . . . 16
β’
β²π₯dist |
46 | 45, 6 | nffv 6848 |
. . . . . . . . . . . . . . 15
β’
β²π₯(distββ¦π¦ / π₯β¦π
) |
47 | 26, 26 | nfxp 5664 |
. . . . . . . . . . . . . . 15
β’
β²π₯(β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π) |
48 | 46, 47 | nfres 5936 |
. . . . . . . . . . . . . 14
β’
β²π₯((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π)) |
49 | | nfcv 2906 |
. . . . . . . . . . . . . . 15
β’
β²π₯βMet |
50 | 49, 26 | nffv 6848 |
. . . . . . . . . . . . . 14
β’
β²π₯(βMetββ¦π¦ / π₯β¦π) |
51 | 48, 50 | nfel 2920 |
. . . . . . . . . . . . 13
β’
β²π₯((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π)) β
(βMetββ¦π¦ / π₯β¦π) |
52 | | prdsdsf.e |
. . . . . . . . . . . . . . 15
β’ πΈ = ((distβπ
) βΎ (π Γ π)) |
53 | 8 | fveq2d 6842 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (distβπ
) = (distββ¦π¦ / π₯β¦π
)) |
54 | 29 | sqxpeqd 5663 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (π Γ π) = (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π)) |
55 | 53, 54 | reseq12d 5935 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β ((distβπ
) βΎ (π Γ π)) = ((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π))) |
56 | 52, 55 | eqtrid 2790 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β πΈ = ((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π))) |
57 | 29 | fveq2d 6842 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β (βMetβπ) = (βMetββ¦π¦ / π₯β¦π)) |
58 | 56, 57 | eleq12d 2833 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (πΈ β (βMetβπ) β ((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π)) β
(βMetββ¦π¦ / π₯β¦π))) |
59 | 51, 58 | rspc 3568 |
. . . . . . . . . . . 12
β’ (π¦ β πΌ β (βπ₯ β πΌ πΈ β (βMetβπ) β ((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π)) β
(βMetββ¦π¦ / π₯β¦π))) |
60 | 44, 59 | mpan9 508 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β ((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π)) β
(βMetββ¦π¦ / π₯β¦π)) |
61 | | xmetcl 23606 |
. . . . . . . . . . 11
β’
((((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π)) β
(βMetββ¦π¦ / π₯β¦π) β§ (πβπ¦) β β¦π¦ / π₯β¦π β§ (πβπ¦) β β¦π¦ / π₯β¦π) β ((πβπ¦)((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π))(πβπ¦)) β
β*) |
62 | 60, 32, 39, 61 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β ((πβπ¦)((distββ¦π¦ / π₯β¦π
) βΎ (β¦π¦ / π₯β¦π Γ β¦π¦ / π₯β¦π))(πβπ¦)) β
β*) |
63 | 41, 62 | eqeltrd 2839 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π¦ β πΌ) β ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦)) β
β*) |
64 | 63 | fmpttd 7058 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))):πΌβΆβ*) |
65 | 64 | frnd 6672 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) β
β*) |
66 | | 0xr 11136 |
. . . . . . . . 9
β’ 0 β
β* |
67 | 66 | a1i 11 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ π β π΅)) β 0 β
β*) |
68 | 67 | snssd 4768 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ π β π΅)) β {0} β
β*) |
69 | 65, 68 | unssd 4145 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β (ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}) β
β*) |
70 | | supxrcl 13163 |
. . . . . 6
β’ ((ran
(π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}) β β*
β sup((ran (π¦ β
πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, < )
β β*) |
71 | 69, 70 | syl 17 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, < )
β β*) |
72 | | ssun2 4132 |
. . . . . . 7
β’ {0}
β (ran (π¦ β
πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}) |
73 | | c0ex 11083 |
. . . . . . . 8
β’ 0 β
V |
74 | 73 | snss 4745 |
. . . . . . 7
β’ (0 β
(ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}) β {0} β (ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0})) |
75 | 72, 74 | mpbir 230 |
. . . . . 6
β’ 0 β
(ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}) |
76 | | supxrub 13172 |
. . . . . 6
β’ (((ran
(π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}) β β*
β§ 0 β (ran (π¦
β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0})) β 0 β€ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, <
)) |
77 | 69, 75, 76 | sylancl 587 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅)) β 0 β€ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, <
)) |
78 | | elxrge0 13303 |
. . . . 5
β’ (sup((ran
(π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, < )
β (0[,]+β) β (sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, < )
β β* β§ 0 β€ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, <
))) |
79 | 71, 77, 78 | sylanbrc 584 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅)) β sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, < )
β (0[,]+β)) |
80 | 79 | ralrimivva 3196 |
. . 3
β’ (π β βπ β π΅ βπ β π΅ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, < )
β (0[,]+β)) |
81 | | eqid 2738 |
. . . 4
β’ (π β π΅, π β π΅ β¦ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, < ))
= (π β π΅, π β π΅ β¦ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, <
)) |
82 | 81 | fmpo 7989 |
. . 3
β’
(βπ β
π΅ βπ β π΅ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, < )
β (0[,]+β) β (π β π΅, π β π΅ β¦ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, <
)):(π΅ Γ π΅)βΆ(0[,]+β)) |
83 | 80, 82 | sylib 217 |
. 2
β’ (π β (π β π΅, π β π΅ β¦ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, <
)):(π΅ Γ π΅)βΆ(0[,]+β)) |
84 | 21 | mptexd 7169 |
. . . 4
β’ (π β (π₯ β πΌ β¦ π
) β V) |
85 | 2 | ralrimiva 3142 |
. . . . 5
β’ (π β βπ₯ β πΌ π
β π) |
86 | | dmmptg 6191 |
. . . . 5
β’
(βπ₯ β
πΌ π
β π β dom (π₯ β πΌ β¦ π
) = πΌ) |
87 | 85, 86 | syl 17 |
. . . 4
β’ (π β dom (π₯ β πΌ β¦ π
) = πΌ) |
88 | | prdsdsf.d |
. . . 4
β’ π· = (distβπ) |
89 | 17, 19, 84, 18, 87, 88 | prdsds 17281 |
. . 3
β’ (π β π· = (π β π΅, π β π΅ β¦ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, <
))) |
90 | 89 | feq1d 6649 |
. 2
β’ (π β (π·:(π΅ Γ π΅)βΆ(0[,]+β) β (π β π΅, π β π΅ β¦ sup((ran (π¦ β πΌ β¦ ((πβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πβπ¦))) βͺ {0}), β*, <
)):(π΅ Γ π΅)βΆ(0[,]+β))) |
91 | 83, 90 | mpbird 257 |
1
β’ (π β π·:(π΅ Γ π΅)βΆ(0[,]+β)) |