Metamath Proof Explorer

Theorem measun

Description: The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017)

Ref Expression
Assertion measun ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑀 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
2 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
3 2 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝑆 ∈ ∪ ran sigAlgebra )
4 simp2l ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ∈ 𝑆 )
5 simp2r ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ∈ 𝑆 )
6 unelsiga ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )
7 3 4 5 6 syl3anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )
8 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
9 8 a1i ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) )
10 measxun2 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ) → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐵 ) +e ( 𝑀 ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐵 ) ) ) )
11 1 7 5 9 10 syl121anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐵 ) +e ( 𝑀 ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐵 ) ) ) )
12 difun2 ⊢ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐵 ) = ( 𝐴 ∖ 𝐵 )
13 uneq1 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = ( ∅ ∪ ( 𝐴 ∖ 𝐵 ) ) )
14 uncom ⊢ ( ∅ ∪ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ∅ )
15 un0 ⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ∅ ) = ( 𝐴 ∖ 𝐵 )
16 14 15 eqtri ⊢ ( ∅ ∪ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
17 13 16 eqtrdi ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 ) )
18 inundif ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
19 17 18 eqtr3di ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∖ 𝐵 ) = 𝐴 )
20 12 19 eqtrid ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐵 ) = 𝐴 )
21 20 fveq2d ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝑀 ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐵 ) ) = ( 𝑀 ‘ 𝐴 ) )
22 21 oveq2d ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝑀 ‘ 𝐵 ) +e ( 𝑀 ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐵 ) ) ) = ( ( 𝑀 ‘ 𝐵 ) +e ( 𝑀 ‘ 𝐴 ) ) )
23 22 3ad2ant3 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝑀 ‘ 𝐵 ) +e ( 𝑀 ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐵 ) ) ) = ( ( 𝑀 ‘ 𝐵 ) +e ( 𝑀 ‘ 𝐴 ) ) )
24 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
25 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
26 24 25 sselid ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐵 ) ∈ ℝ* )
27 1 5 26 syl2anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑀 ‘ 𝐵 ) ∈ ℝ* )
28 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
29 24 28 sselid ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
30 1 4 29 syl2anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
31 xaddcom ⊢ ( ( ( 𝑀 ‘ 𝐵 ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝐴 ) ∈ ℝ* ) → ( ( 𝑀 ‘ 𝐵 ) +e ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑀 ‘ 𝐵 ) ) )
32 27 30 31 syl2anc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝑀 ‘ 𝐵 ) +e ( 𝑀 ‘ 𝐴 ) ) = ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑀 ‘ 𝐵 ) ) )
33 11 23 32 3eqtrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑀 ‘ 𝐵 ) ) )