Step | Hyp | Ref
| Expression |
1 | | simp1 1134 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π β (measuresβπ)) |
2 | | simp3l 1199 |
. . . . . 6
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π΄ βΌ Ο) |
3 | | measvunilem.1 |
. . . . . . 7
β’
β²π₯π΄ |
4 | 3 | abrexctf 32210 |
. . . . . 6
β’ (π΄ βΌ Ο β {π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο) |
5 | 2, 4 | syl 17 |
. . . . 5
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο) |
6 | | ctex 8961 |
. . . . 5
β’ ({π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β V) |
7 | 5, 6 | syl 17 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β V) |
8 | | simp2 1135 |
. . . . 5
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βπ₯ β π΄ π΅ β (π β {β
})) |
9 | | eldifi 4125 |
. . . . . . 7
β’ (π΅ β (π β {β
}) β π΅ β π) |
10 | 9 | ralimi 3081 |
. . . . . 6
β’
(βπ₯ β
π΄ π΅ β (π β {β
}) β βπ₯ β π΄ π΅ β π) |
11 | | nfcv 2901 |
. . . . . . 7
β’
β²π₯π |
12 | 11 | abrexss 32016 |
. . . . . 6
β’
(βπ₯ β
π΄ π΅ β π β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π) |
13 | 10, 12 | syl 17 |
. . . . 5
β’
(βπ₯ β
π΄ π΅ β (π β {β
}) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π) |
14 | 8, 13 | syl 17 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π) |
15 | | elpwg 4604 |
. . . . 5
β’ ({π¦ β£ βπ₯ β π΄ π¦ = π΅} β V β ({π¦ β£ βπ₯ β π΄ π¦ = π΅} β π« π β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π)) |
16 | 15 | biimpar 476 |
. . . 4
β’ (({π¦ β£ βπ₯ β π΄ π¦ = π΅} β V β§ {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π« π) |
17 | 7, 14, 16 | syl2anc 582 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π« π) |
18 | | simp3r 1200 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Disj π₯ β π΄ π΅) |
19 | 3 | disjabrexf 32081 |
. . . 4
β’
(Disj π₯
β π΄ π΅ β Disj π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅}π§) |
20 | 18, 19 | syl 17 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Disj π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅}π§) |
21 | | measvun 33505 |
. . 3
β’ ((π β (measuresβπ) β§ {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π« π β§ ({π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο β§ Disj π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅}π§)) β (πββͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅}) = Ξ£*π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅} (πβπ§)) |
22 | 1, 17, 5, 20, 21 | syl112anc 1372 |
. 2
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅}) = Ξ£*π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅} (πβπ§)) |
23 | | dfiun2g 5032 |
. . . 4
β’
(βπ₯ β
π΄ π΅ β (π β {β
}) β βͺ π₯ β π΄ π΅ = βͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅}) |
24 | 23 | fveq2d 6894 |
. . 3
β’
(βπ₯ β
π΄ π΅ β (π β {β
}) β (πββͺ π₯ β π΄ π΅) = (πββͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅})) |
25 | 8, 24 | syl 17 |
. 2
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β π΄ π΅) = (πββͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅})) |
26 | | nfcv 2901 |
. . 3
β’
β²π₯(πβπ§) |
27 | | nfv 1915 |
. . . 4
β’
β²π₯ π β (measuresβπ) |
28 | | nfra1 3279 |
. . . 4
β’
β²π₯βπ₯ β π΄ π΅ β (π β {β
}) |
29 | | nfcv 2901 |
. . . . . 6
β’
β²π₯
βΌ |
30 | | nfcv 2901 |
. . . . . 6
β’
β²π₯Ο |
31 | 3, 29, 30 | nfbr 5194 |
. . . . 5
β’
β²π₯ π΄ βΌ
Ο |
32 | | nfdisj1 5126 |
. . . . 5
β’
β²π₯Disj
π₯ β π΄ π΅ |
33 | 31, 32 | nfan 1900 |
. . . 4
β’
β²π₯(π΄ βΌ Ο β§
Disj π₯ β π΄ π΅) |
34 | 27, 28, 33 | nf3an 1902 |
. . 3
β’
β²π₯(π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) |
35 | | fveq2 6890 |
. . 3
β’ (π§ = π΅ β (πβπ§) = (πβπ΅)) |
36 | | ctex 8961 |
. . . 4
β’ (π΄ βΌ Ο β π΄ β V) |
37 | 2, 36 | syl 17 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π΄ β V) |
38 | 8 | r19.21bi 3246 |
. . . 4
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β π΄) β π΅ β (π β {β
})) |
39 | 34, 3, 38, 18 | disjdsct 32191 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Fun β‘(π₯ β π΄ β¦ π΅)) |
40 | | simpl1 1189 |
. . . 4
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β π΄) β π β (measuresβπ)) |
41 | | measvxrge0 33501 |
. . . . 5
β’ ((π β (measuresβπ) β§ π΅ β π) β (πβπ΅) β (0[,]+β)) |
42 | 9, 41 | sylan2 591 |
. . . 4
β’ ((π β (measuresβπ) β§ π΅ β (π β {β
})) β (πβπ΅) β (0[,]+β)) |
43 | 40, 38, 42 | syl2anc 582 |
. . 3
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β π΄) β (πβπ΅) β (0[,]+β)) |
44 | 26, 34, 3, 35, 37, 39, 43, 38 | esumc 33347 |
. 2
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Ξ£*π₯ β π΄(πβπ΅) = Ξ£*π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅} (πβπ§)) |
45 | 22, 25, 44 | 3eqtr4d 2780 |
1
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β π΄ π΅) = Ξ£*π₯ β π΄(πβπ΅)) |