Step | Hyp | Ref
| Expression |
1 | | prdsbasmpt2.y |
. . 3
β’ π = (πXs(π₯ β πΌ β¦ π
)) |
2 | | prdsbasmpt2.b |
. . 3
β’ π΅ = (Baseβπ) |
3 | | prdsbasmpt2.s |
. . 3
β’ (π β π β π) |
4 | | prdsbasmpt2.i |
. . 3
β’ (π β πΌ β π) |
5 | | prdsbasmpt2.r |
. . . 4
β’ (π β βπ₯ β πΌ π
β π) |
6 | | eqid 2737 |
. . . . 5
β’ (π₯ β πΌ β¦ π
) = (π₯ β πΌ β¦ π
) |
7 | 6 | fnmpt 6642 |
. . . 4
β’
(βπ₯ β
πΌ π
β π β (π₯ β πΌ β¦ π
) Fn πΌ) |
8 | 5, 7 | syl 17 |
. . 3
β’ (π β (π₯ β πΌ β¦ π
) Fn πΌ) |
9 | | prdsdsval2.f |
. . 3
β’ (π β πΉ β π΅) |
10 | | prdsdsval2.g |
. . 3
β’ (π β πΊ β π΅) |
11 | | prdsdsval2.d |
. . 3
β’ π· = (distβπ) |
12 | 1, 2, 3, 4, 8, 9, 10, 11 | prdsdsval 17361 |
. 2
β’ (π β (πΉπ·πΊ) = sup((ran (π¦ β πΌ β¦ ((πΉβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πΊβπ¦))) βͺ {0}), β*, <
)) |
13 | | nfcv 2908 |
. . . . . . . 8
β’
β²π₯(πΉβπ¦) |
14 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π₯dist |
15 | | nffvmpt1 6854 |
. . . . . . . . 9
β’
β²π₯((π₯ β πΌ β¦ π
)βπ¦) |
16 | 14, 15 | nffv 6853 |
. . . . . . . 8
β’
β²π₯(distβ((π₯ β πΌ β¦ π
)βπ¦)) |
17 | | nfcv 2908 |
. . . . . . . 8
β’
β²π₯(πΊβπ¦) |
18 | 13, 16, 17 | nfov 7388 |
. . . . . . 7
β’
β²π₯((πΉβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πΊβπ¦)) |
19 | | nfcv 2908 |
. . . . . . 7
β’
β²π¦((πΉβπ₯)(distβ((π₯ β πΌ β¦ π
)βπ₯))(πΊβπ₯)) |
20 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π¦ = π₯ β (distβ((π₯ β πΌ β¦ π
)βπ¦)) = (distβ((π₯ β πΌ β¦ π
)βπ₯))) |
21 | | fveq2 6843 |
. . . . . . . 8
β’ (π¦ = π₯ β (πΉβπ¦) = (πΉβπ₯)) |
22 | | fveq2 6843 |
. . . . . . . 8
β’ (π¦ = π₯ β (πΊβπ¦) = (πΊβπ₯)) |
23 | 20, 21, 22 | oveq123d 7379 |
. . . . . . 7
β’ (π¦ = π₯ β ((πΉβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πΊβπ¦)) = ((πΉβπ₯)(distβ((π₯ β πΌ β¦ π
)βπ₯))(πΊβπ₯))) |
24 | 18, 19, 23 | cbvmpt 5217 |
. . . . . 6
β’ (π¦ β πΌ β¦ ((πΉβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πΊβπ¦))) = (π₯ β πΌ β¦ ((πΉβπ₯)(distβ((π₯ β πΌ β¦ π
)βπ₯))(πΊβπ₯))) |
25 | | eqidd 2738 |
. . . . . . 7
β’ (π β πΌ = πΌ) |
26 | 6 | fvmpt2 6960 |
. . . . . . . . . . . 12
β’ ((π₯ β πΌ β§ π
β π) β ((π₯ β πΌ β¦ π
)βπ₯) = π
) |
27 | 26 | fveq2d 6847 |
. . . . . . . . . . 11
β’ ((π₯ β πΌ β§ π
β π) β (distβ((π₯ β πΌ β¦ π
)βπ₯)) = (distβπ
)) |
28 | | prdsdsval2.e |
. . . . . . . . . . 11
β’ πΈ = (distβπ
) |
29 | 27, 28 | eqtr4di 2795 |
. . . . . . . . . 10
β’ ((π₯ β πΌ β§ π
β π) β (distβ((π₯ β πΌ β¦ π
)βπ₯)) = πΈ) |
30 | 29 | oveqd 7375 |
. . . . . . . . 9
β’ ((π₯ β πΌ β§ π
β π) β ((πΉβπ₯)(distβ((π₯ β πΌ β¦ π
)βπ₯))(πΊβπ₯)) = ((πΉβπ₯)πΈ(πΊβπ₯))) |
31 | 30 | ralimiaa 3086 |
. . . . . . . 8
β’
(βπ₯ β
πΌ π
β π β βπ₯ β πΌ ((πΉβπ₯)(distβ((π₯ β πΌ β¦ π
)βπ₯))(πΊβπ₯)) = ((πΉβπ₯)πΈ(πΊβπ₯))) |
32 | 5, 31 | syl 17 |
. . . . . . 7
β’ (π β βπ₯ β πΌ ((πΉβπ₯)(distβ((π₯ β πΌ β¦ π
)βπ₯))(πΊβπ₯)) = ((πΉβπ₯)πΈ(πΊβπ₯))) |
33 | | mpteq12 5198 |
. . . . . . 7
β’ ((πΌ = πΌ β§ βπ₯ β πΌ ((πΉβπ₯)(distβ((π₯ β πΌ β¦ π
)βπ₯))(πΊβπ₯)) = ((πΉβπ₯)πΈ(πΊβπ₯))) β (π₯ β πΌ β¦ ((πΉβπ₯)(distβ((π₯ β πΌ β¦ π
)βπ₯))(πΊβπ₯))) = (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯)))) |
34 | 25, 32, 33 | syl2anc 585 |
. . . . . 6
β’ (π β (π₯ β πΌ β¦ ((πΉβπ₯)(distβ((π₯ β πΌ β¦ π
)βπ₯))(πΊβπ₯))) = (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯)))) |
35 | 24, 34 | eqtrid 2789 |
. . . . 5
β’ (π β (π¦ β πΌ β¦ ((πΉβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πΊβπ¦))) = (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯)))) |
36 | 35 | rneqd 5894 |
. . . 4
β’ (π β ran (π¦ β πΌ β¦ ((πΉβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πΊβπ¦))) = ran (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯)))) |
37 | 36 | uneq1d 4123 |
. . 3
β’ (π β (ran (π¦ β πΌ β¦ ((πΉβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πΊβπ¦))) βͺ {0}) = (ran (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯))) βͺ {0})) |
38 | 37 | supeq1d 9383 |
. 2
β’ (π β sup((ran (π¦ β πΌ β¦ ((πΉβπ¦)(distβ((π₯ β πΌ β¦ π
)βπ¦))(πΊβπ¦))) βͺ {0}), β*, < ) =
sup((ran (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯))) βͺ {0}), β*, <
)) |
39 | 12, 38 | eqtrd 2777 |
1
β’ (π β (πΉπ·πΊ) = sup((ran (π₯ β πΌ β¦ ((πΉβπ₯)πΈ(πΊβπ₯))) βͺ {0}), β*, <
)) |