Metamath Proof Explorer

Theorem measxun2

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

Ref Expression
Assertion measxun2 
|- ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( M ` A ) = ( ( M ` B ) +e ( M ` ( A \ B ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> M e. ( measures ` S ) )
2 simp2r 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> B e. S )
3 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
4 1 3 syl 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> S e. U. ran sigAlgebra )
5 simp2l 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> A e. S )
6 difelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )
7 4 5 2 6 syl3anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( A \ B ) e. S )
8 prelpwi 
 |-  ( ( B e. S /\ ( A \ B ) e. S ) -> { B , ( A \ B ) } e. ~P S )
9 2 7 8 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> { B , ( A \ B ) } e. ~P S )
10 prct 
 |-  ( ( B e. S /\ ( A \ B ) e. S ) -> { B , ( A \ B ) } ~<_ _om )
11 2 7 10 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> { B , ( A \ B ) } ~<_ _om )
12 simp3 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> B C_ A )
13 disjdifprg2 
 |-  ( A e. S -> Disj_ x e. { ( A \ B ) , ( A i^i B ) } x )
14 prcom 
 |-  { ( A \ B ) , B } = { B , ( A \ B ) }
15 dfss 
 |-  ( B C_ A <-> B = ( B i^i A ) )
16 15 biimpi 
 |-  ( B C_ A -> B = ( B i^i A ) )
17 incom 
 |-  ( B i^i A ) = ( A i^i B )
18 16 17 eqtrdi 
 |-  ( B C_ A -> B = ( A i^i B ) )
19 18 preq2d 
 |-  ( B C_ A -> { ( A \ B ) , B } = { ( A \ B ) , ( A i^i B ) } )
20 14 19 eqtr3id 
 |-  ( B C_ A -> { B , ( A \ B ) } = { ( A \ B ) , ( A i^i B ) } )
21 20 disjeq1d 
 |-  ( B C_ A -> ( Disj_ x e. { B , ( A \ B ) } x <-> Disj_ x e. { ( A \ B ) , ( A i^i B ) } x ) )
22 21 biimprd 
 |-  ( B C_ A -> ( Disj_ x e. { ( A \ B ) , ( A i^i B ) } x -> Disj_ x e. { B , ( A \ B ) } x ) )
23 13 22 mpan9 
 |-  ( ( A e. S /\ B C_ A ) -> Disj_ x e. { B , ( A \ B ) } x )
24 5 12 23 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> Disj_ x e. { B , ( A \ B ) } x )
25 11 24 jca 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( { B , ( A \ B ) } ~<_ _om /\ Disj_ x e. { B , ( A \ B ) } x ) )
26 measvun 
 |-  ( ( M e. ( measures ` S ) /\ { B , ( A \ B ) } e. ~P S /\ ( { B , ( A \ B ) } ~<_ _om /\ Disj_ x e. { B , ( A \ B ) } x ) ) -> ( M ` U. { B , ( A \ B ) } ) = sum* x e. { B , ( A \ B ) } ( M ` x ) )
27 1 9 25 26 syl3anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( M ` U. { B , ( A \ B ) } ) = sum* x e. { B , ( A \ B ) } ( M ` x ) )
28 2 7 jca 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( B e. S /\ ( A \ B ) e. S ) )
29 uniprg 
 |-  ( ( B e. S /\ ( A \ B ) e. S ) -> U. { B , ( A \ B ) } = ( B u. ( A \ B ) ) )
30 undif 
 |-  ( B C_ A <-> ( B u. ( A \ B ) ) = A )
31 30 biimpi 
 |-  ( B C_ A -> ( B u. ( A \ B ) ) = A )
32 29 31 sylan9eq 
 |-  ( ( ( B e. S /\ ( A \ B ) e. S ) /\ B C_ A ) -> U. { B , ( A \ B ) } = A )
33 32 fveq2d 
 |-  ( ( ( B e. S /\ ( A \ B ) e. S ) /\ B C_ A ) -> ( M ` U. { B , ( A \ B ) } ) = ( M ` A ) )
34 28 12 33 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( M ` U. { B , ( A \ B ) } ) = ( M ` A ) )
35 simpr 
 |-  ( ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) /\ x = B ) -> x = B )
36 35 fveq2d 
 |-  ( ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) /\ x = B ) -> ( M ` x ) = ( M ` B ) )
37 simpr 
 |-  ( ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) /\ x = ( A \ B ) ) -> x = ( A \ B ) )
38 37 fveq2d 
 |-  ( ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) /\ x = ( A \ B ) ) -> ( M ` x ) = ( M ` ( A \ B ) ) )
39 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ B e. S ) -> ( M ` B ) e. ( 0 [,] +oo ) )
40 1 2 39 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( M ` B ) e. ( 0 [,] +oo ) )
41 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ ( A \ B ) e. S ) -> ( M ` ( A \ B ) ) e. ( 0 [,] +oo ) )
42 1 7 41 syl2anc 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( M ` ( A \ B ) ) e. ( 0 [,] +oo ) )
43 eqimss 
 |-  ( B = ( A \ B ) -> B C_ ( A \ B ) )
44 ssdifeq0 
 |-  ( B C_ ( A \ B ) <-> B = (/) )
45 43 44 sylib 
 |-  ( B = ( A \ B ) -> B = (/) )
46 45 fveq2d 
 |-  ( B = ( A \ B ) -> ( M ` B ) = ( M ` (/) ) )
47 measvnul 
 |-  ( M e. ( measures ` S ) -> ( M ` (/) ) = 0 )
48 46 47 sylan9eqr 
 |-  ( ( M e. ( measures ` S ) /\ B = ( A \ B ) ) -> ( M ` B ) = 0 )
49 1 48 sylan 
 |-  ( ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) /\ B = ( A \ B ) ) -> ( M ` B ) = 0 )
50 49 orcd 
 |-  ( ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) /\ B = ( A \ B ) ) -> ( ( M ` B ) = 0 \/ ( M ` B ) = +oo ) )
51 50 ex 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( B = ( A \ B ) -> ( ( M ` B ) = 0 \/ ( M ` B ) = +oo ) ) )
52 36 38 2 7 40 42 51 esumpr2 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> sum* x e. { B , ( A \ B ) } ( M ` x ) = ( ( M ` B ) +e ( M ` ( A \ B ) ) ) )
53 27 34 52 3eqtr3d 
 |-  ( ( M e. ( measures ` S ) /\ ( A e. S /\ B e. S ) /\ B C_ A ) -> ( M ` A ) = ( ( M ` B ) +e ( M ` ( A \ B ) ) ) )