Step | Hyp | Ref
| Expression |
1 | | sitmval.1 |
. . 3
β’ (π β π β π) |
2 | | elex 3461 |
. . 3
β’ (π β π β π β V) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β π β V) |
4 | | sitmval.2 |
. 2
β’ (π β π β βͺ ran
measures) |
5 | | oveq1 7358 |
. . . . 5
β’ (π€ = π β (π€sitgπ) = (πsitgπ)) |
6 | 5 | dmeqd 5859 |
. . . 4
β’ (π€ = π β dom (π€sitgπ) = dom (πsitgπ)) |
7 | | fveq2 6839 |
. . . . . . 7
β’ (π€ = π β (distβπ€) = (distβπ)) |
8 | 7 | ofeqd 7611 |
. . . . . 6
β’ (π€ = π β βf
(distβπ€) =
βf (distβπ)) |
9 | 8 | oveqd 7368 |
. . . . 5
β’ (π€ = π β (π βf (distβπ€)π) = (π βf (distβπ)π)) |
10 | 9 | fveq2d 6843 |
. . . 4
β’ (π€ = π β
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ€)π)) =
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ)π))) |
11 | 6, 6, 10 | mpoeq123dv 7426 |
. . 3
β’ (π€ = π β (π β dom (π€sitgπ), π β dom (π€sitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ€)π))) = (π β dom (πsitgπ), π β dom (πsitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ)π)))) |
12 | | oveq2 7359 |
. . . . 5
β’ (π = π β (πsitgπ) = (πsitgπ)) |
13 | 12 | dmeqd 5859 |
. . . 4
β’ (π = π β dom (πsitgπ) = dom (πsitgπ)) |
14 | | oveq2 7359 |
. . . . 5
β’ (π = π β
((β*π βΎs
(0[,]+β))sitgπ) =
((β*π βΎs
(0[,]+β))sitgπ)) |
15 | | sitmval.d |
. . . . . . . 8
β’ π· = (distβπ) |
16 | 15 | eqcomi 2746 |
. . . . . . 7
β’
(distβπ) =
π· |
17 | | ofeq 7612 |
. . . . . . 7
β’
((distβπ) =
π· β
βf (distβπ) = βf π·) |
18 | 16, 17 | mp1i 13 |
. . . . . 6
β’ (π = π β βf
(distβπ) =
βf π·) |
19 | 18 | oveqd 7368 |
. . . . 5
β’ (π = π β (π βf (distβπ)π) = (π βf π·π)) |
20 | 14, 19 | fveq12d 6846 |
. . . 4
β’ (π = π β
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ)π)) =
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf π·π))) |
21 | 13, 13, 20 | mpoeq123dv 7426 |
. . 3
β’ (π = π β (π β dom (πsitgπ), π β dom (πsitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ)π))) = (π β dom (πsitgπ), π β dom (πsitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf π·π)))) |
22 | | df-sitm 32743 |
. . 3
β’ sitm =
(π€ β V, π β βͺ ran measures β¦ (π β dom (π€sitgπ), π β dom (π€sitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf (distβπ€)π)))) |
23 | | ovex 7384 |
. . . . 5
β’ (πsitgπ) β V |
24 | 23 | dmex 7840 |
. . . 4
β’ dom
(πsitgπ) β V |
25 | 24, 24 | mpoex 8004 |
. . 3
β’ (π β dom (πsitgπ), π β dom (πsitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf π·π))) β V |
26 | 11, 21, 22, 25 | ovmpo 7509 |
. 2
β’ ((π β V β§ π β βͺ ran measures) β (πsitmπ) = (π β dom (πsitgπ), π β dom (πsitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf π·π)))) |
27 | 3, 4, 26 | syl2anc 584 |
1
β’ (π β (πsitmπ) = (π β dom (πsitgπ), π β dom (πsitgπ) β¦
(((β*π βΎs
(0[,]+β))sitgπ)β(π βf π·π)))) |