Step | Hyp | Ref
| Expression |
1 | | simp2 1138 |
. 2
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β π β βͺ ran
sigAlgebra) |
2 | | measfrge0 33201 |
. . . . 5
β’ (π β (measuresβπ) β π:πβΆ(0[,]+β)) |
3 | 2 | 3ad2ant1 1134 |
. . . 4
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β π:πβΆ(0[,]+β)) |
4 | | simp3 1139 |
. . . 4
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β π β π) |
5 | 3, 4 | fssresd 6759 |
. . 3
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β (π βΎ π):πβΆ(0[,]+β)) |
6 | | 0elsiga 33112 |
. . . . 5
β’ (π β βͺ ran sigAlgebra β β
β π) |
7 | | fvres 6911 |
. . . . 5
β’ (β
β π β ((π βΎ π)ββ
) = (πββ
)) |
8 | 1, 6, 7 | 3syl 18 |
. . . 4
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β ((π βΎ π)ββ
) = (πββ
)) |
9 | | measvnul 33204 |
. . . . 5
β’ (π β (measuresβπ) β (πββ
) = 0) |
10 | 9 | 3ad2ant1 1134 |
. . . 4
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β (πββ
) =
0) |
11 | 8, 10 | eqtrd 2773 |
. . 3
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β ((π βΎ π)ββ
) = 0) |
12 | | simp11 1204 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β π β (measuresβπ)) |
13 | | simp13 1206 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β π β π) |
14 | | simp2 1138 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β π₯ β π« π) |
15 | | sspw 4614 |
. . . . . . . . 9
β’ (π β π β π« π β π« π) |
16 | 15 | sselda 3983 |
. . . . . . . 8
β’ ((π β π β§ π₯ β π« π) β π₯ β π« π) |
17 | 13, 14, 16 | syl2anc 585 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β π₯ β π« π) |
18 | | simp3 1139 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) |
19 | | measvun 33207 |
. . . . . . 7
β’ ((π β (measuresβπ) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)) |
20 | 12, 17, 18, 19 | syl3anc 1372 |
. . . . . 6
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β (πββͺ π₯) = Ξ£*π¦ β π₯(πβπ¦)) |
21 | 1 | 3ad2ant1 1134 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β π β βͺ ran
sigAlgebra) |
22 | | simp3l 1202 |
. . . . . . . 8
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β π₯ βΌ Ο) |
23 | | sigaclcu 33115 |
. . . . . . . 8
β’ ((π β βͺ ran sigAlgebra β§ π₯ β π« π β§ π₯ βΌ Ο) β βͺ π₯
β π) |
24 | 21, 14, 22, 23 | syl3anc 1372 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β βͺ π₯ β π) |
25 | 24 | fvresd 6912 |
. . . . . 6
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β ((π βΎ π)ββͺ π₯) = (πββͺ π₯)) |
26 | | elpwi 4610 |
. . . . . . . . . . 11
β’ (π₯ β π« π β π₯ β π) |
27 | 26 | sselda 3983 |
. . . . . . . . . 10
β’ ((π₯ β π« π β§ π¦ β π₯) β π¦ β π) |
28 | 27 | adantll 713 |
. . . . . . . . 9
β’ ((((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π) β§ π¦ β π₯) β π¦ β π) |
29 | 28 | fvresd 6912 |
. . . . . . . 8
β’ ((((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π) β§ π¦ β π₯) β ((π βΎ π)βπ¦) = (πβπ¦)) |
30 | 29 | esumeq2dv 33036 |
. . . . . . 7
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π) β Ξ£*π¦ β π₯((π βΎ π)βπ¦) = Ξ£*π¦ β π₯(πβπ¦)) |
31 | 30 | 3adant3 1133 |
. . . . . 6
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β Ξ£*π¦ β π₯((π βΎ π)βπ¦) = Ξ£*π¦ β π₯(πβπ¦)) |
32 | 20, 25, 31 | 3eqtr4d 2783 |
. . . . 5
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β ((π βΎ π)ββͺ π₯) = Ξ£*π¦ β π₯((π βΎ π)βπ¦)) |
33 | 32 | 3expia 1122 |
. . . 4
β’ (((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β§ π₯ β π« π) β ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β ((π βΎ π)ββͺ π₯) = Ξ£*π¦ β π₯((π βΎ π)βπ¦))) |
34 | 33 | ralrimiva 3147 |
. . 3
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β βπ₯ β π« π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β ((π βΎ π)ββͺ π₯) = Ξ£*π¦ β π₯((π βΎ π)βπ¦))) |
35 | 5, 11, 34 | 3jca 1129 |
. 2
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β ((π βΎ π):πβΆ(0[,]+β) β§ ((π βΎ π)ββ
) = 0 β§ βπ₯ β π« π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β ((π βΎ π)ββͺ π₯) = Ξ£*π¦ β π₯((π βΎ π)βπ¦)))) |
36 | | ismeas 33197 |
. . 3
β’ (π β βͺ ran sigAlgebra β ((π βΎ π) β (measuresβπ) β ((π βΎ π):πβΆ(0[,]+β) β§ ((π βΎ π)ββ
) = 0 β§ βπ₯ β π« π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β ((π βΎ π)ββͺ π₯) = Ξ£*π¦ β π₯((π βΎ π)βπ¦))))) |
37 | 36 | biimprd 247 |
. 2
β’ (π β βͺ ran sigAlgebra β (((π βΎ π):πβΆ(0[,]+β) β§ ((π βΎ π)ββ
) = 0 β§ βπ₯ β π« π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β ((π βΎ π)ββͺ π₯) = Ξ£*π¦ β π₯((π βΎ π)βπ¦))) β (π βΎ π) β (measuresβπ))) |
38 | 1, 35, 37 | sylc 65 |
1
β’ ((π β (measuresβπ) β§ π β βͺ ran
sigAlgebra β§ π β
π) β (π βΎ π) β (measuresβπ)) |