Step | Hyp | Ref
| Expression |
1 | | df-oms 33291 |
. 2
β’ toOMeas =
(π β V β¦ (π β π« βͺ dom π β¦ inf(ran (π₯ β {π§ β π« dom π β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(πβπ¦)), (0[,]+β), < ))) |
2 | | dmeq 5904 |
. . . . 5
β’ (π = π
β dom π = dom π
) |
3 | 2 | unieqd 4923 |
. . . 4
β’ (π = π
β βͺ dom
π = βͺ dom π
) |
4 | 3 | pweqd 4620 |
. . 3
β’ (π = π
β π« βͺ dom π = π« βͺ dom
π
) |
5 | 2 | pweqd 4620 |
. . . . . . 7
β’ (π = π
β π« dom π = π« dom π
) |
6 | | rabeq 3447 |
. . . . . . 7
β’
(π« dom π =
π« dom π
β
{π§ β π« dom
π β£ (π β βͺ π§
β§ π§ βΌ Ο)} =
{π§ β π« dom
π
β£ (π β βͺ π§
β§ π§ βΌ
Ο)}) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (π = π
β {π§ β π« dom π β£ (π β βͺ π§ β§ π§ βΌ Ο)} = {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)}) |
8 | | simpl 484 |
. . . . . . . 8
β’ ((π = π
β§ π¦ β π₯) β π = π
) |
9 | 8 | fveq1d 6894 |
. . . . . . 7
β’ ((π = π
β§ π¦ β π₯) β (πβπ¦) = (π
βπ¦)) |
10 | 9 | esumeq2dv 33036 |
. . . . . 6
β’ (π = π
β Ξ£*π¦ β π₯(πβπ¦) = Ξ£*π¦ β π₯(π
βπ¦)) |
11 | 7, 10 | mpteq12dv 5240 |
. . . . 5
β’ (π = π
β (π₯ β {π§ β π« dom π β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(πβπ¦)) = (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦))) |
12 | 11 | rneqd 5938 |
. . . 4
β’ (π = π
β ran (π₯ β {π§ β π« dom π β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(πβπ¦)) = ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦))) |
13 | 12 | infeq1d 9472 |
. . 3
β’ (π = π
β inf(ran (π₯ β {π§ β π« dom π β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(πβπ¦)), (0[,]+β), < ) = inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) |
14 | 4, 13 | mpteq12dv 5240 |
. 2
β’ (π = π
β (π β π« βͺ dom π β¦ inf(ran (π₯ β {π§ β π« dom π β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(πβπ¦)), (0[,]+β), < )) = (π β π« βͺ dom π
β¦ inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < ))) |
15 | | id 22 |
. 2
β’ (π
β V β π
β V) |
16 | | dmexg 7894 |
. . 3
β’ (π
β V β dom π
β V) |
17 | | uniexg 7730 |
. . 3
β’ (dom
π
β V β βͺ dom π
β V) |
18 | | pwexg 5377 |
. . 3
β’ (βͺ dom π
β V β π« βͺ dom π
β V) |
19 | | mptexg 7223 |
. . 3
β’
(π« βͺ dom π
β V β (π β π« βͺ dom π
β¦ inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) β
V) |
20 | 16, 17, 18, 19 | 4syl 19 |
. 2
β’ (π
β V β (π β π« βͺ dom π
β¦ inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < )) β
V) |
21 | 1, 14, 15, 20 | fvmptd3 7022 |
1
β’ (π
β V β
(toOMeasβπ
) = (π β π« βͺ dom π
β¦ inf(ran (π₯ β {π§ β π« dom π
β£ (π β βͺ π§ β§ π§ βΌ Ο)} β¦
Ξ£*π¦ β
π₯(π
βπ¦)), (0[,]+β), < ))) |