Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π β (measuresβπ)) |
2 | | simp3l 1202 |
. . . . . 6
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π΄ βΌ Ο) |
3 | | measvunilem.1 |
. . . . . . 7
β’
β²π₯π΄ |
4 | 3 | abrexctf 31689 |
. . . . . 6
β’ (π΄ βΌ Ο β {π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο) |
5 | 2, 4 | syl 17 |
. . . . 5
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο) |
6 | | ctex 8909 |
. . . . 5
β’ ({π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β V) |
7 | 5, 6 | syl 17 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β V) |
8 | | simp2 1138 |
. . . . 5
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βπ₯ β π΄ π΅ β (π β {β
})) |
9 | | eldifi 4090 |
. . . . . . 7
β’ (π΅ β (π β {β
}) β π΅ β π) |
10 | 9 | ralimi 3083 |
. . . . . 6
β’
(βπ₯ β
π΄ π΅ β (π β {β
}) β βπ₯ β π΄ π΅ β π) |
11 | | nfcv 2904 |
. . . . . . 7
β’
β²π₯π |
12 | 11 | abrexss 31488 |
. . . . . 6
β’
(βπ₯ β
π΄ π΅ β π β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π) |
13 | 10, 12 | syl 17 |
. . . . 5
β’
(βπ₯ β
π΄ π΅ β (π β {β
}) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π) |
14 | 8, 13 | syl 17 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π) |
15 | | elpwg 4567 |
. . . . 5
β’ ({π¦ β£ βπ₯ β π΄ π¦ = π΅} β V β ({π¦ β£ βπ₯ β π΄ π¦ = π΅} β π« π β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π)) |
16 | 15 | biimpar 479 |
. . . 4
β’ (({π¦ β£ βπ₯ β π΄ π¦ = π΅} β V β§ {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π« π) |
17 | 7, 14, 16 | syl2anc 585 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π« π) |
18 | | simp3r 1203 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Disj π₯ β π΄ π΅) |
19 | 3 | disjabrexf 31554 |
. . . 4
β’
(Disj π₯
β π΄ π΅ β Disj π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅}π§) |
20 | 18, 19 | syl 17 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Disj π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅}π§) |
21 | | measvun 32872 |
. . 3
β’ ((π β (measuresβπ) β§ {π¦ β£ βπ₯ β π΄ π¦ = π΅} β π« π β§ ({π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο β§ Disj π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅}π§)) β (πββͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅}) = Ξ£*π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅} (πβπ§)) |
22 | 1, 17, 5, 20, 21 | syl112anc 1375 |
. 2
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅}) = Ξ£*π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅} (πβπ§)) |
23 | | dfiun2g 4994 |
. . . 4
β’
(βπ₯ β
π΄ π΅ β (π β {β
}) β βͺ π₯ β π΄ π΅ = βͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅}) |
24 | 23 | fveq2d 6850 |
. . 3
β’
(βπ₯ β
π΄ π΅ β (π β {β
}) β (πββͺ π₯ β π΄ π΅) = (πββͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅})) |
25 | 8, 24 | syl 17 |
. 2
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β π΄ π΅) = (πββͺ {π¦ β£ βπ₯ β π΄ π¦ = π΅})) |
26 | | nfcv 2904 |
. . 3
β’
β²π₯(πβπ§) |
27 | | nfv 1918 |
. . . 4
β’
β²π₯ π β (measuresβπ) |
28 | | nfra1 3266 |
. . . 4
β’
β²π₯βπ₯ β π΄ π΅ β (π β {β
}) |
29 | | nfcv 2904 |
. . . . . 6
β’
β²π₯
βΌ |
30 | | nfcv 2904 |
. . . . . 6
β’
β²π₯Ο |
31 | 3, 29, 30 | nfbr 5156 |
. . . . 5
β’
β²π₯ π΄ βΌ
Ο |
32 | | nfdisj1 5088 |
. . . . 5
β’
β²π₯Disj
π₯ β π΄ π΅ |
33 | 31, 32 | nfan 1903 |
. . . 4
β’
β²π₯(π΄ βΌ Ο β§
Disj π₯ β π΄ π΅) |
34 | 27, 28, 33 | nf3an 1905 |
. . 3
β’
β²π₯(π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) |
35 | | fveq2 6846 |
. . 3
β’ (π§ = π΅ β (πβπ§) = (πβπ΅)) |
36 | | ctex 8909 |
. . . 4
β’ (π΄ βΌ Ο β π΄ β V) |
37 | 2, 36 | syl 17 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π΄ β V) |
38 | 8 | r19.21bi 3233 |
. . . 4
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β π΄) β π΅ β (π β {β
})) |
39 | 34, 3, 38, 18 | disjdsct 31670 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Fun β‘(π₯ β π΄ β¦ π΅)) |
40 | | simpl1 1192 |
. . . 4
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β π΄) β π β (measuresβπ)) |
41 | | measvxrge0 32868 |
. . . . 5
β’ ((π β (measuresβπ) β§ π΅ β π) β (πβπ΅) β (0[,]+β)) |
42 | 9, 41 | sylan2 594 |
. . . 4
β’ ((π β (measuresβπ) β§ π΅ β (π β {β
})) β (πβπ΅) β (0[,]+β)) |
43 | 40, 38, 42 | syl2anc 585 |
. . 3
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β π΄) β (πβπ΅) β (0[,]+β)) |
44 | 26, 34, 3, 35, 37, 39, 43, 38 | esumc 32714 |
. 2
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Ξ£*π₯ β π΄(πβπ΅) = Ξ£*π§ β {π¦ β£ βπ₯ β π΄ π¦ = π΅} (πβπ§)) |
45 | 22, 25, 44 | 3eqtr4d 2783 |
1
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β (π β {β
}) β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β π΄ π΅) = Ξ£*π₯ β π΄(πβπ΅)) |