Description: The measure of the union of two disjoint sets, with finite measure, is the sum of the measures, Property 112C (a) of Fremlin1 p. 15. (Contributed by Glauco Siliprandi, 8-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | meadjunre.m | |- ( ph -> M e. Meas ) |
|
| meadjunre.x | |- S = dom M |
||
| meadjunre.a | |- ( ph -> A e. S ) |
||
| meadjunre.b | |- ( ph -> B e. S ) |
||
| meadjunre.d | |- ( ph -> ( A i^i B ) = (/) ) |
||
| meadjunre.r | |- ( ph -> ( M ` A ) e. RR ) |
||
| meadjunre.f | |- ( ph -> ( M ` B ) e. RR ) |
||
| Assertion | meadjunre | |- ( ph -> ( M ` ( A u. B ) ) = ( ( M ` A ) + ( M ` B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | meadjunre.m | |- ( ph -> M e. Meas ) |
|
| 2 | meadjunre.x | |- S = dom M |
|
| 3 | meadjunre.a | |- ( ph -> A e. S ) |
|
| 4 | meadjunre.b | |- ( ph -> B e. S ) |
|
| 5 | meadjunre.d | |- ( ph -> ( A i^i B ) = (/) ) |
|
| 6 | meadjunre.r | |- ( ph -> ( M ` A ) e. RR ) |
|
| 7 | meadjunre.f | |- ( ph -> ( M ` B ) e. RR ) |
|
| 8 | 1 2 3 4 5 | meadjun | |- ( ph -> ( M ` ( A u. B ) ) = ( ( M ` A ) +e ( M ` B ) ) ) |
| 9 | 6 7 | rexaddd | |- ( ph -> ( ( M ` A ) +e ( M ` B ) ) = ( ( M ` A ) + ( M ` B ) ) ) |
| 10 | 8 9 | eqtrd | |- ( ph -> ( M ` ( A u. B ) ) = ( ( M ` A ) + ( M ` B ) ) ) |