Step | Hyp | Ref
| Expression |
1 | | simp2 1137 |
. 2
β’ ((π β (measuresβπ) β§ π΄ β π« π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π₯)) β π΄ β π« π) |
2 | | measbase 33481 |
. . . . . 6
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
3 | | ismeas 33483 |
. . . . . 6
β’ (π β βͺ ran sigAlgebra β (π β (measuresβπ) β (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ¦ β π«
π((π¦ βΌ Ο β§ Disj π₯ β π¦ π₯) β (πββͺ π¦) = Ξ£*π₯ β π¦(πβπ₯))))) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ (π β (measuresβπ) β (π β (measuresβπ) β (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ¦ β π«
π((π¦ βΌ Ο β§ Disj π₯ β π¦ π₯) β (πββͺ π¦) = Ξ£*π₯ β π¦(πβπ₯))))) |
5 | 4 | ibi 266 |
. . . 4
β’ (π β (measuresβπ) β (π:πβΆ(0[,]+β) β§ (πββ
) = 0 β§
βπ¦ β π«
π((π¦ βΌ Ο β§ Disj π₯ β π¦ π₯) β (πββͺ π¦) = Ξ£*π₯ β π¦(πβπ₯)))) |
6 | 5 | simp3d 1144 |
. . 3
β’ (π β (measuresβπ) β βπ¦ β π« π((π¦ βΌ Ο β§ Disj π₯ β π¦ π₯) β (πββͺ π¦) = Ξ£*π₯ β π¦(πβπ₯))) |
7 | 6 | 3ad2ant1 1133 |
. 2
β’ ((π β (measuresβπ) β§ π΄ β π« π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π₯)) β βπ¦ β π« π((π¦ βΌ Ο β§ Disj π₯ β π¦ π₯) β (πββͺ π¦) = Ξ£*π₯ β π¦(πβπ₯))) |
8 | | simp3 1138 |
. 2
β’ ((π β (measuresβπ) β§ π΄ β π« π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π₯)) β (π΄ βΌ Ο β§ Disj π₯ β π΄ π₯)) |
9 | | breq1 5151 |
. . . . 5
β’ (π¦ = π΄ β (π¦ βΌ Ο β π΄ βΌ Ο)) |
10 | | disjeq1 5120 |
. . . . 5
β’ (π¦ = π΄ β (Disj π₯ β π¦ π₯ β Disj π₯ β π΄ π₯)) |
11 | 9, 10 | anbi12d 631 |
. . . 4
β’ (π¦ = π΄ β ((π¦ βΌ Ο β§ Disj π₯ β π¦ π₯) β (π΄ βΌ Ο β§ Disj π₯ β π΄ π₯))) |
12 | | unieq 4919 |
. . . . . 6
β’ (π¦ = π΄ β βͺ π¦ = βͺ
π΄) |
13 | 12 | fveq2d 6895 |
. . . . 5
β’ (π¦ = π΄ β (πββͺ π¦) = (πββͺ π΄)) |
14 | | esumeq1 33318 |
. . . . 5
β’ (π¦ = π΄ β Ξ£*π₯ β π¦(πβπ₯) = Ξ£*π₯ β π΄(πβπ₯)) |
15 | 13, 14 | eqeq12d 2748 |
. . . 4
β’ (π¦ = π΄ β ((πββͺ π¦) = Ξ£*π₯ β π¦(πβπ₯) β (πββͺ π΄) = Ξ£*π₯ β π΄(πβπ₯))) |
16 | 11, 15 | imbi12d 344 |
. . 3
β’ (π¦ = π΄ β (((π¦ βΌ Ο β§ Disj π₯ β π¦ π₯) β (πββͺ π¦) = Ξ£*π₯ β π¦(πβπ₯)) β ((π΄ βΌ Ο β§ Disj π₯ β π΄ π₯) β (πββͺ π΄) = Ξ£*π₯ β π΄(πβπ₯)))) |
17 | 16 | rspcv 3608 |
. 2
β’ (π΄ β π« π β (βπ¦ β π« π((π¦ βΌ Ο β§ Disj π₯ β π¦ π₯) β (πββͺ π¦) = Ξ£*π₯ β π¦(πβπ₯)) β ((π΄ βΌ Ο β§ Disj π₯ β π΄ π₯) β (πββͺ π΄) = Ξ£*π₯ β π΄(πβπ₯)))) |
18 | 1, 7, 8, 17 | syl3c 66 |
1
β’ ((π β (measuresβπ) β§ π΄ β π« π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π₯)) β (πββͺ π΄) = Ξ£*π₯ β π΄(πβπ₯)) |