Step | Hyp | Ref
| Expression |
1 | | df-metu 20818 |
. 2
β’ metUnif =
(π β βͺ ran PsMet β¦ ((dom dom π Γ dom dom π)filGenran (π β β+ β¦ (β‘π β (0[,)π))))) |
2 | | simpr 486 |
. . . . . . 7
β’ ((π· β (PsMetβπ) β§ π = π·) β π = π·) |
3 | 2 | dmeqd 5865 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π = π·) β dom π = dom π·) |
4 | 3 | dmeqd 5865 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π = π·) β dom dom π = dom dom π·) |
5 | | psmetdmdm 23681 |
. . . . . 6
β’ (π· β (PsMetβπ) β π = dom dom π·) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π = π·) β π = dom dom π·) |
7 | 4, 6 | eqtr4d 2776 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π = π·) β dom dom π = π) |
8 | 7 | sqxpeqd 5669 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β (dom dom π Γ dom dom π) = (π Γ π)) |
9 | | simplr 768 |
. . . . . . 7
β’ (((π· β (PsMetβπ) β§ π = π·) β§ π β β+) β π = π·) |
10 | 9 | cnveqd 5835 |
. . . . . 6
β’ (((π· β (PsMetβπ) β§ π = π·) β§ π β β+) β β‘π = β‘π·) |
11 | 10 | imaeq1d 6016 |
. . . . 5
β’ (((π· β (PsMetβπ) β§ π = π·) β§ π β β+) β (β‘π β (0[,)π)) = (β‘π· β (0[,)π))) |
12 | 11 | mpteq2dva 5209 |
. . . 4
β’ ((π· β (PsMetβπ) β§ π = π·) β (π β β+ β¦ (β‘π β (0[,)π))) = (π β β+ β¦ (β‘π· β (0[,)π)))) |
13 | 12 | rneqd 5897 |
. . 3
β’ ((π· β (PsMetβπ) β§ π = π·) β ran (π β β+ β¦ (β‘π β (0[,)π))) = ran (π β β+ β¦ (β‘π· β (0[,)π)))) |
14 | 8, 13 | oveq12d 7379 |
. 2
β’ ((π· β (PsMetβπ) β§ π = π·) β ((dom dom π Γ dom dom π)filGenran (π β β+ β¦ (β‘π β (0[,)π)))) = ((π Γ π)filGenran (π β β+ β¦ (β‘π· β (0[,)π))))) |
15 | | elfvunirn 6878 |
. 2
β’ (π· β (PsMetβπ) β π· β βͺ ran
PsMet) |
16 | | ovexd 7396 |
. 2
β’ (π· β (PsMetβπ) β ((π Γ π)filGenran (π β β+ β¦ (β‘π· β (0[,)π)))) β V) |
17 | 1, 14, 15, 16 | fvmptd2 6960 |
1
β’ (π· β (PsMetβπ) β (metUnifβπ·) = ((π Γ π)filGenran (π β β+ β¦ (β‘π· β (0[,)π))))) |