Step | Hyp | Ref
| Expression |
1 | | df-metu 20942 |
. 2
β’ metUnif =
(π β βͺ ran PsMet β¦ ((dom dom π Γ dom dom π)filGenran (π β β+ β¦ (β‘π β (0[,)π))))) |
2 | | simpr 485 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π = π·) β π = π·) |
3 | 2 | dmeqd 5905 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π = π·) β dom π = dom π·) |
4 | 3 | dmeqd 5905 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π = π·) β dom dom π = dom dom π·) |
5 | | psmetdmdm 23810 |
. . . . . 6
β’ (π· β (PsMetβπ) β π = dom dom π·) |
6 | 5 | adantr 481 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π = π·) β π = dom dom π·) |
7 | 4, 6 | eqtr4d 2775 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π = π·) β dom dom π = π) |
8 | 7 | sqxpeqd 5708 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β (dom dom π Γ dom dom π) = (π Γ π)) |
9 | | simplr 767 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π = π·) β§ π β β+) β π = π·) |
10 | 9 | cnveqd 5875 |
. . . . . 6
β’ (((π· β (PsMetβπ) β§ π = π·) β§ π β β+) β β‘π = β‘π·) |
11 | 10 | imaeq1d 6058 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π = π·) β§ π β β+) β (β‘π β (0[,)π)) = (β‘π· β (0[,)π))) |
12 | 11 | mpteq2dva 5248 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π = π·) β (π β β+ β¦ (β‘π β (0[,)π))) = (π β β+ β¦ (β‘π· β (0[,)π)))) |
13 | 12 | rneqd 5937 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β ran (π β β+ β¦ (β‘π β (0[,)π))) = ran (π β β+ β¦ (β‘π· β (0[,)π)))) |
14 | 8, 13 | oveq12d 7426 |
. 2
β’ ((π· β (PsMetβπ) β§ π = π·) β ((dom dom π Γ dom dom π)filGenran (π β β+ β¦ (β‘π β (0[,)π)))) = ((π Γ π)filGenran (π β β+ β¦ (β‘π· β (0[,)π))))) |
15 | | elfvunirn 6923 |
. 2
β’ (π· β (PsMetβπ) β π· β βͺ ran
PsMet) |
16 | | ovexd 7443 |
. 2
β’ (π· β (PsMetβπ) β ((π Γ π)filGenran (π β β+ β¦ (β‘π· β (0[,)π)))) β V) |
17 | 1, 14, 15, 16 | fvmptd2 7006 |
1
β’ (π· β (PsMetβπ) β (metUnifβπ·) = ((π Γ π)filGenran (π β β+ β¦ (β‘π· β (0[,)π))))) |