Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π β (measuresβπ)) |
2 | | rabid 3452 |
. . . . . . . 8
β’ (π₯ β {π₯ β π΄ β£ π΅ β {β
}} β (π₯ β π΄ β§ π΅ β {β
})) |
3 | 2 | simprbi 497 |
. . . . . . 7
β’ (π₯ β {π₯ β π΄ β£ π΅ β {β
}} β π΅ β {β
}) |
4 | 3 | adantl 482 |
. . . . . 6
β’ ((π β (measuresβπ) β§ π₯ β {π₯ β π΄ β£ π΅ β {β
}}) β π΅ β {β
}) |
5 | 4 | ralrimiva 3146 |
. . . . 5
β’ (π β (measuresβπ) β βπ₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β {β
}) |
6 | 5 | 3ad2ant1 1133 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βπ₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β {β
}) |
7 | | ssrab2 4076 |
. . . . . . 7
β’ {π₯ β π΄ β£ π΅ β {β
}} β π΄ |
8 | | ssct 9047 |
. . . . . . 7
β’ (({π₯ β π΄ β£ π΅ β {β
}} β π΄ β§ π΄ βΌ Ο) β {π₯ β π΄ β£ π΅ β {β
}} βΌ
Ο) |
9 | 7, 8 | mpan 688 |
. . . . . 6
β’ (π΄ βΌ Ο β {π₯ β π΄ β£ π΅ β {β
}} βΌ
Ο) |
10 | 9 | adantr 481 |
. . . . 5
β’ ((π΄ βΌ Ο β§
Disj π₯ β π΄ π΅) β {π₯ β π΄ β£ π΅ β {β
}} βΌ
Ο) |
11 | 10 | 3ad2ant3 1135 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π₯ β π΄ β£ π΅ β {β
}} βΌ
Ο) |
12 | | simp3r 1202 |
. . . . 5
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Disj π₯ β π΄ π΅) |
13 | | nfrab1 3451 |
. . . . . 6
β’
β²π₯{π₯ β π΄ β£ π΅ β {β
}} |
14 | | nfcv 2903 |
. . . . . 6
β’
β²π₯π΄ |
15 | 13, 14 | disjss1f 31790 |
. . . . 5
β’ ({π₯ β π΄ β£ π΅ β {β
}} β π΄ β (Disj π₯ β π΄ π΅ β Disj π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅)) |
16 | 7, 12, 15 | mpsyl 68 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Disj π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅) |
17 | 13 | measvunilem0 33199 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β {β
} β§ ({π₯ β π΄ β£ π΅ β {β
}} βΌ Ο β§
Disj π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅)) β (πββͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅) = Ξ£*π₯ β {π₯ β π΄ β£ π΅ β {β
}} (πβπ΅)) |
18 | 1, 6, 11, 16, 17 | syl112anc 1374 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅) = Ξ£*π₯ β {π₯ β π΄ β£ π΅ β {β
}} (πβπ΅)) |
19 | | rabid 3452 |
. . . . . . . 8
β’ (π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})} β (π₯ β π΄ β§ π΅ β (π β {β
}))) |
20 | 19 | simprbi 497 |
. . . . . . 7
β’ (π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})} β π΅ β (π β {β
})) |
21 | 20 | adantl 482 |
. . . . . 6
β’ ((π β (measuresβπ) β§ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}) β π΅ β (π β {β
})) |
22 | 21 | ralrimiva 3146 |
. . . . 5
β’ (π β (measuresβπ) β βπ₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅ β (π β {β
})) |
23 | 22 | 3ad2ant1 1133 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βπ₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅ β (π β {β
})) |
24 | | ssrab2 4076 |
. . . . . . 7
β’ {π₯ β π΄ β£ π΅ β (π β {β
})} β π΄ |
25 | | ssct 9047 |
. . . . . . 7
β’ (({π₯ β π΄ β£ π΅ β (π β {β
})} β π΄ β§ π΄ βΌ Ο) β {π₯ β π΄ β£ π΅ β (π β {β
})} βΌ
Ο) |
26 | 24, 25 | mpan 688 |
. . . . . 6
β’ (π΄ βΌ Ο β {π₯ β π΄ β£ π΅ β (π β {β
})} βΌ
Ο) |
27 | 26 | adantr 481 |
. . . . 5
β’ ((π΄ βΌ Ο β§
Disj π₯ β π΄ π΅) β {π₯ β π΄ β£ π΅ β (π β {β
})} βΌ
Ο) |
28 | 27 | 3ad2ant3 1135 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π₯ β π΄ β£ π΅ β (π β {β
})} βΌ
Ο) |
29 | | nfrab1 3451 |
. . . . . 6
β’
β²π₯{π₯ β π΄ β£ π΅ β (π β {β
})} |
30 | 29, 14 | disjss1f 31790 |
. . . . 5
β’ ({π₯ β π΄ β£ π΅ β (π β {β
})} β π΄ β (Disj π₯ β π΄ π΅ β Disj π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅)) |
31 | 24, 12, 30 | mpsyl 68 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Disj π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅) |
32 | 29 | measvunilem 33198 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅ β (π β {β
}) β§ ({π₯ β π΄ β£ π΅ β (π β {β
})} βΌ Ο β§
Disj π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅)) β (πββͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅) = Ξ£*π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})} (πβπ΅)) |
33 | 1, 23, 28, 31, 32 | syl112anc 1374 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅) = Ξ£*π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})} (πβπ΅)) |
34 | 18, 33 | oveq12d 7423 |
. 2
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β ((πββͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅) +π (πββͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅)) = (Ξ£*π₯ β {π₯ β π΄ β£ π΅ β {β
}} (πβπ΅) +π
Ξ£*π₯ β
{π₯ β π΄ β£ π΅ β (π β {β
})} (πβπ΅))) |
35 | | nfv 1917 |
. . . . . . 7
β’
β²π₯ π β (measuresβπ) |
36 | | nfra1 3281 |
. . . . . . 7
β’
β²π₯βπ₯ β π΄ π΅ β π |
37 | | nfv 1917 |
. . . . . . . 8
β’
β²π₯ π΄ βΌ
Ο |
38 | | nfdisj1 5126 |
. . . . . . . 8
β’
β²π₯Disj
π₯ β π΄ π΅ |
39 | 37, 38 | nfan 1902 |
. . . . . . 7
β’
β²π₯(π΄ βΌ Ο β§
Disj π₯ β π΄ π΅) |
40 | 35, 36, 39 | nf3an 1904 |
. . . . . 6
β’
β²π₯(π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) |
41 | 13, 29 | nfun 4164 |
. . . . . 6
β’
β²π₯({π₯ β π΄ β£ π΅ β {β
}} βͺ {π₯ β π΄ β£ π΅ β (π β {β
})}) |
42 | | simp2 1137 |
. . . . . . . . 9
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βπ₯ β π΄ π΅ β π) |
43 | | rabid2 3464 |
. . . . . . . . 9
β’ (π΄ = {π₯ β π΄ β£ π΅ β π} β βπ₯ β π΄ π΅ β π) |
44 | 42, 43 | sylibr 233 |
. . . . . . . 8
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π΄ = {π₯ β π΄ β£ π΅ β π}) |
45 | | elun 4147 |
. . . . . . . . . . 11
β’ (π΅ β ({β
} βͺ (π β {β
})) β
(π΅ β {β
} β¨
π΅ β (π β {β
}))) |
46 | | measbase 33183 |
. . . . . . . . . . . . . 14
β’ (π β (measuresβπ) β π β βͺ ran
sigAlgebra) |
47 | | 0elsiga 33100 |
. . . . . . . . . . . . . 14
β’ (π β βͺ ran sigAlgebra β β
β π) |
48 | | snssi 4810 |
. . . . . . . . . . . . . 14
β’ (β
β π β {β
}
β π) |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β (measuresβπ) β {β
} β π) |
50 | | undif 4480 |
. . . . . . . . . . . . 13
β’
({β
} β π
β ({β
} βͺ (π
β {β
})) = π) |
51 | 49, 50 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β (measuresβπ) β ({β
} βͺ (π β {β
})) = π) |
52 | 51 | eleq2d 2819 |
. . . . . . . . . . 11
β’ (π β (measuresβπ) β (π΅ β ({β
} βͺ (π β {β
})) β π΅ β π)) |
53 | 45, 52 | bitr3id 284 |
. . . . . . . . . 10
β’ (π β (measuresβπ) β ((π΅ β {β
} β¨ π΅ β (π β {β
})) β π΅ β π)) |
54 | 53 | rabbidv 3440 |
. . . . . . . . 9
β’ (π β (measuresβπ) β {π₯ β π΄ β£ (π΅ β {β
} β¨ π΅ β (π β {β
}))} = {π₯ β π΄ β£ π΅ β π}) |
55 | 54 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π₯ β π΄ β£ (π΅ β {β
} β¨ π΅ β (π β {β
}))} = {π₯ β π΄ β£ π΅ β π}) |
56 | 44, 55 | eqtr4d 2775 |
. . . . . . 7
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π΄ = {π₯ β π΄ β£ (π΅ β {β
} β¨ π΅ β (π β {β
}))}) |
57 | | unrab 4304 |
. . . . . . 7
β’ ({π₯ β π΄ β£ π΅ β {β
}} βͺ {π₯ β π΄ β£ π΅ β (π β {β
})}) = {π₯ β π΄ β£ (π΅ β {β
} β¨ π΅ β (π β {β
}))} |
58 | 56, 57 | eqtr4di 2790 |
. . . . . 6
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π΄ = ({π₯ β π΄ β£ π΅ β {β
}} βͺ {π₯ β π΄ β£ π΅ β (π β {β
})})) |
59 | | eqidd 2733 |
. . . . . 6
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π΅ = π΅) |
60 | 40, 14, 41, 58, 59 | iuneq12df 5022 |
. . . . 5
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βͺ π₯ β π΄ π΅ = βͺ π₯ β ({π₯ β π΄ β£ π΅ β {β
}} βͺ {π₯ β π΄ β£ π΅ β (π β {β
})})π΅) |
61 | 60 | fveq2d 6892 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β π΄ π΅) = (πββͺ
π₯ β ({π₯ β π΄ β£ π΅ β {β
}} βͺ {π₯ β π΄ β£ π΅ β (π β {β
})})π΅)) |
62 | | iunxun 5096 |
. . . . 5
β’ βͺ π₯ β ({π₯ β π΄ β£ π΅ β {β
}} βͺ {π₯ β π΄ β£ π΅ β (π β {β
})})π΅ = (βͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ βͺ βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅) |
63 | 62 | fveq2i 6891 |
. . . 4
β’ (πββͺ π₯ β ({π₯ β π΄ β£ π΅ β {β
}} βͺ {π₯ β π΄ β£ π΅ β (π β {β
})})π΅) = (πβ(βͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ βͺ βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅)) |
64 | 61, 63 | eqtrdi 2788 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β π΄ π΅) = (πβ(βͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ βͺ βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅))) |
65 | 46 | 3ad2ant1 1133 |
. . . . 5
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β π β βͺ ran
sigAlgebra) |
66 | 47 | adantr 481 |
. . . . . . . . 9
β’ ((π β βͺ ran sigAlgebra β§ π΅ β {β
}) β β
β
π) |
67 | | elsni 4644 |
. . . . . . . . . . 11
β’ (π΅ β {β
} β π΅ = β
) |
68 | 67 | eleq1d 2818 |
. . . . . . . . . 10
β’ (π΅ β {β
} β (π΅ β π β β
β π)) |
69 | 68 | adantl 482 |
. . . . . . . . 9
β’ ((π β βͺ ran sigAlgebra β§ π΅ β {β
}) β (π΅ β π β β
β π)) |
70 | 66, 69 | mpbird 256 |
. . . . . . . 8
β’ ((π β βͺ ran sigAlgebra β§ π΅ β {β
}) β π΅ β π) |
71 | 46, 3, 70 | syl2an 596 |
. . . . . . 7
β’ ((π β (measuresβπ) β§ π₯ β {π₯ β π΄ β£ π΅ β {β
}}) β π΅ β π) |
72 | 71 | ralrimiva 3146 |
. . . . . 6
β’ (π β (measuresβπ) β βπ₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β π) |
73 | 72 | 3ad2ant1 1133 |
. . . . 5
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βπ₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β π) |
74 | 13 | sigaclcuni 33104 |
. . . . 5
β’ ((π β βͺ ran sigAlgebra β§ βπ₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β π β§ {π₯ β π΄ β£ π΅ β {β
}} βΌ Ο) β
βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β π) |
75 | 65, 73, 11, 74 | syl3anc 1371 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β π) |
76 | 21 | eldifad 3959 |
. . . . . . 7
β’ ((π β (measuresβπ) β§ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}) β π΅ β π) |
77 | 76 | ralrimiva 3146 |
. . . . . 6
β’ (π β (measuresβπ) β βπ₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅ β π) |
78 | 77 | 3ad2ant1 1133 |
. . . . 5
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βπ₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅ β π) |
79 | 29 | sigaclcuni 33104 |
. . . . 5
β’ ((π β βͺ ran sigAlgebra β§ βπ₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅ β π β§ {π₯ β π΄ β£ π΅ β (π β {β
})} βΌ Ο) β
βͺ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅ β π) |
80 | 65, 78, 28, 79 | syl3anc 1371 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β βͺ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅ β π) |
81 | 3, 67 | syl 17 |
. . . . . . 7
β’ (π₯ β {π₯ β π΄ β£ π΅ β {β
}} β π΅ = β
) |
82 | 81 | iuneq2i 5017 |
. . . . . 6
β’ βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ = βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}β
|
83 | | iun0 5064 |
. . . . . 6
β’ βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}β
=
β
|
84 | 82, 83 | eqtri 2760 |
. . . . 5
β’ βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ = β
|
85 | | ineq1 4204 |
. . . . . 6
β’ (βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ = β
β (βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β© βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅) = (β
β© βͺ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅)) |
86 | | 0in 4392 |
. . . . . 6
β’ (β
β© βͺ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅) = β
|
87 | 85, 86 | eqtrdi 2788 |
. . . . 5
β’ (βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ = β
β (βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β© βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅) = β
) |
88 | 84, 87 | mp1i 13 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β© βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅) = β
) |
89 | | measun 33197 |
. . . 4
β’ ((π β (measuresβπ) β§ (βͺ π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β π β§ βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅ β π) β§ (βͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ β© βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅) = β
) β (πβ(βͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ βͺ βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅)) = ((πββͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅) +π (πββͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅))) |
90 | 1, 75, 80, 88, 89 | syl121anc 1375 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πβ(βͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅ βͺ βͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅)) = ((πββͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅) +π (πββͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅))) |
91 | 64, 90 | eqtrd 2772 |
. 2
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β π΄ π΅) = ((πββͺ
π₯ β {π₯ β π΄ β£ π΅ β {β
}}π΅) +π (πββͺ
π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}π΅))) |
92 | 40, 58 | esumeq1d 33021 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Ξ£*π₯ β π΄(πβπ΅) = Ξ£*π₯ β ({π₯ β π΄ β£ π΅ β {β
}} βͺ {π₯ β π΄ β£ π΅ β (π β {β
})})(πβπ΅)) |
93 | | ctex 8955 |
. . . . 5
β’ ({π₯ β π΄ β£ π΅ β {β
}} βΌ Ο β
{π₯ β π΄ β£ π΅ β {β
}} β
V) |
94 | 11, 93 | syl 17 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π₯ β π΄ β£ π΅ β {β
}} β
V) |
95 | | ctex 8955 |
. . . . 5
β’ ({π₯ β π΄ β£ π΅ β (π β {β
})} βΌ Ο β
{π₯ β π΄ β£ π΅ β (π β {β
})} β
V) |
96 | 28, 95 | syl 17 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β {π₯ β π΄ β£ π΅ β (π β {β
})} β
V) |
97 | | inrab 4305 |
. . . . . 6
β’ ({π₯ β π΄ β£ π΅ β {β
}} β© {π₯ β π΄ β£ π΅ β (π β {β
})}) = {π₯ β π΄ β£ (π΅ β {β
} β§ π΅ β (π β {β
}))} |
98 | | noel 4329 |
. . . . . . . . . 10
β’ Β¬
π΅ β
β
|
99 | | disjdif 4470 |
. . . . . . . . . . 11
β’
({β
} β© (π
β {β
})) = β
|
100 | 99 | eleq2i 2825 |
. . . . . . . . . 10
β’ (π΅ β ({β
} β© (π β {β
})) β
π΅ β
β
) |
101 | 98, 100 | mtbir 322 |
. . . . . . . . 9
β’ Β¬
π΅ β ({β
} β©
(π β
{β
})) |
102 | | elin 3963 |
. . . . . . . . 9
β’ (π΅ β ({β
} β© (π β {β
})) β
(π΅ β {β
} β§
π΅ β (π β {β
}))) |
103 | 101, 102 | mtbi 321 |
. . . . . . . 8
β’ Β¬
(π΅ β {β
} β§
π΅ β (π β {β
})) |
104 | 103 | rgenw 3065 |
. . . . . . 7
β’
βπ₯ β
π΄ Β¬ (π΅ β {β
} β§ π΅ β (π β {β
})) |
105 | | rabeq0 4383 |
. . . . . . 7
β’ ({π₯ β π΄ β£ (π΅ β {β
} β§ π΅ β (π β {β
}))} = β
β
βπ₯ β π΄ Β¬ (π΅ β {β
} β§ π΅ β (π β {β
}))) |
106 | 104, 105 | mpbir 230 |
. . . . . 6
β’ {π₯ β π΄ β£ (π΅ β {β
} β§ π΅ β (π β {β
}))} =
β
|
107 | 97, 106 | eqtri 2760 |
. . . . 5
β’ ({π₯ β π΄ β£ π΅ β {β
}} β© {π₯ β π΄ β£ π΅ β (π β {β
})}) =
β
|
108 | 107 | a1i 11 |
. . . 4
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β ({π₯ β π΄ β£ π΅ β {β
}} β© {π₯ β π΄ β£ π΅ β (π β {β
})}) =
β
) |
109 | 1 | adantr 481 |
. . . . 5
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β {π₯ β π΄ β£ π΅ β {β
}}) β π β (measuresβπ)) |
110 | 1, 71 | sylan 580 |
. . . . 5
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β {π₯ β π΄ β£ π΅ β {β
}}) β π΅ β π) |
111 | | measvxrge0 33191 |
. . . . 5
β’ ((π β (measuresβπ) β§ π΅ β π) β (πβπ΅) β (0[,]+β)) |
112 | 109, 110,
111 | syl2anc 584 |
. . . 4
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β {π₯ β π΄ β£ π΅ β {β
}}) β (πβπ΅) β (0[,]+β)) |
113 | 1 | adantr 481 |
. . . . 5
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}) β π β (measuresβπ)) |
114 | 20 | adantl 482 |
. . . . . 6
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}) β π΅ β (π β {β
})) |
115 | 114 | eldifad 3959 |
. . . . 5
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}) β π΅ β π) |
116 | 113, 115,
111 | syl2anc 584 |
. . . 4
β’ (((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β§ π₯ β {π₯ β π΄ β£ π΅ β (π β {β
})}) β (πβπ΅) β (0[,]+β)) |
117 | 40, 13, 29, 94, 96, 108, 112, 116 | esumsplit 33039 |
. . 3
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Ξ£*π₯ β ({π₯ β π΄ β£ π΅ β {β
}} βͺ {π₯ β π΄ β£ π΅ β (π β {β
})})(πβπ΅) = (Ξ£*π₯ β {π₯ β π΄ β£ π΅ β {β
}} (πβπ΅) +π
Ξ£*π₯ β
{π₯ β π΄ β£ π΅ β (π β {β
})} (πβπ΅))) |
118 | 92, 117 | eqtrd 2772 |
. 2
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β Ξ£*π₯ β π΄(πβπ΅) = (Ξ£*π₯ β {π₯ β π΄ β£ π΅ β {β
}} (πβπ΅) +π
Ξ£*π₯ β
{π₯ β π΄ β£ π΅ β (π β {β
})} (πβπ΅))) |
119 | 34, 91, 118 | 3eqtr4d 2782 |
1
β’ ((π β (measuresβπ) β§ βπ₯ β π΄ π΅ β π β§ (π΄ βΌ Ο β§ Disj π₯ β π΄ π΅)) β (πββͺ
π₯ β π΄ π΅) = Ξ£*π₯ β π΄(πβπ΅)) |