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 
|- ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> ( M ` ( A u. B ) ) = ( ( M ` A ) +e ( M ` B ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> M e. ( measures ` S ) )
2 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
3 2 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> S e. U. ran sigAlgebra )
4 simp2l 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> A e. S )
5 simp2r 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> B e. S )
6 unelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A u. B ) e. S )
7 3 4 5 6 syl3anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> ( A u. B ) e. S )
8 ssun2 
 |-  B C_ ( A u. B )
9 8 a1i 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> B C_ ( A u. B ) )
10 measxun2 
 |-  ( ( M e. ( measures ` S ) /\ ( ( A u. B ) e. S /\ B e. S ) /\ B C_ ( A u. B ) ) -> ( M ` ( A u. B ) ) = ( ( M ` B ) +e ( M ` ( ( A u. B ) \ B ) ) ) )
11 1 7 5 9 10 syl121anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> ( M ` ( A u. B ) ) = ( ( M ` B ) +e ( M ` ( ( A u. B ) \ B ) ) ) )
12 difun2 
 |-  ( ( A u. B ) \ B ) = ( A \ B )
13 uneq1 
 |-  ( ( A i^i B ) = (/) -> ( ( A i^i B ) u. ( A \ B ) ) = ( (/) u. ( A \ B ) ) )
14 uncom 
 |-  ( (/) u. ( A \ B ) ) = ( ( A \ B ) u. (/) )
15 un0 
 |-  ( ( A \ B ) u. (/) ) = ( A \ B )
16 14 15 eqtri 
 |-  ( (/) u. ( A \ B ) ) = ( A \ B )
17 13 16 eqtrdi 
 |-  ( ( A i^i B ) = (/) -> ( ( A i^i B ) u. ( A \ B ) ) = ( A \ B ) )
18 inundif 
 |-  ( ( A i^i B ) u. ( A \ B ) ) = A
19 17 18 eqtr3di 
 |-  ( ( A i^i B ) = (/) -> ( A \ B ) = A )
20 12 19 syl5eq 
 |-  ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A )
21 20 fveq2d 
 |-  ( ( A i^i B ) = (/) -> ( M ` ( ( A u. B ) \ B ) ) = ( M ` A ) )
22 21 oveq2d 
 |-  ( ( A i^i B ) = (/) -> ( ( M ` B ) +e ( M ` ( ( A u. B ) \ B ) ) ) = ( ( M ` B ) +e ( M ` A ) ) )
23 22 3ad2ant3 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> ( ( M ` B ) +e ( M ` ( ( A u. B ) \ B ) ) ) = ( ( M ` B ) +e ( M ` A ) ) )
24 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
25 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ B e. S ) -> ( M ` B ) e. ( 0 [,] +oo ) )
26 24 25 sselid 
 |-  ( ( M e. ( measures ` S ) /\ B e. S ) -> ( M ` B ) e. RR* )
27 1 5 26 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> ( M ` B ) e. RR* )
28 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( M ` A ) e. ( 0 [,] +oo ) )
29 24 28 sselid 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( M ` A ) e. RR* )
30 1 4 29 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> ( M ` A ) e. RR* )
31 xaddcom 
 |-  ( ( ( M ` B ) e. RR* /\ ( M ` A ) e. RR* ) -> ( ( M ` B ) +e ( M ` A ) ) = ( ( M ` A ) +e ( M ` B ) ) )
32 27 30 31 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> ( ( M ` B ) +e ( M ` A ) ) = ( ( M ` A ) +e ( M ` B ) ) )
33 11 23 32 3eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ ( A i^i B ) = (/) ) -> ( M ` ( A u. B ) ) = ( ( M ` A ) +e ( M ` B ) ) )