Metamath Proof Explorer

Theorem volun

Description: The Lebesgue measure function is finitely additive. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion volun 
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> A e. dom vol )
2 mblss 
 |-  ( A e. dom vol -> A C_ RR )
3 1 2 syl 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> A C_ RR )
4 simpl2 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> B e. dom vol )
5 mblss 
 |-  ( B e. dom vol -> B C_ RR )
6 4 5 syl 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> B C_ RR )
7 3 6 unssd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( A u. B ) C_ RR )
8 readdcl 
 |-  ( ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR )
9 8 adantl 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR )
10 simprl 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` A ) e. RR )
11 simprr 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` B ) e. RR )
12 ovolun 
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) )
13 3 10 6 11 12 syl22anc 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) )
14 ovollecl 
 |-  ( ( ( A u. B ) C_ RR /\ ( ( vol* ` A ) + ( vol* ` B ) ) e. RR /\ ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) ) -> ( vol* ` ( A u. B ) ) e. RR )
15 7 9 13 14 syl3anc 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) e. RR )
16 mblsplit 
 |-  ( ( A e. dom vol /\ ( A u. B ) C_ RR /\ ( vol* ` ( A u. B ) ) e. RR ) -> ( vol* ` ( A u. B ) ) = ( ( vol* ` ( ( A u. B ) i^i A ) ) + ( vol* ` ( ( A u. B ) \ A ) ) ) )
17 1 7 15 16 syl3anc 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) = ( ( vol* ` ( ( A u. B ) i^i A ) ) + ( vol* ` ( ( A u. B ) \ A ) ) ) )
18 simpl3 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( A i^i B ) = (/) )
19 indir 
 |-  ( ( A u. B ) i^i A ) = ( ( A i^i A ) u. ( B i^i A ) )
20 inidm 
 |-  ( A i^i A ) = A
21 incom 
 |-  ( B i^i A ) = ( A i^i B )
22 20 21 uneq12i 
 |-  ( ( A i^i A ) u. ( B i^i A ) ) = ( A u. ( A i^i B ) )
23 unabs 
 |-  ( A u. ( A i^i B ) ) = A
24 22 23 eqtri 
 |-  ( ( A i^i A ) u. ( B i^i A ) ) = A
25 19 24 eqtri 
 |-  ( ( A u. B ) i^i A ) = A
26 25 a1i 
 |-  ( ( A i^i B ) = (/) -> ( ( A u. B ) i^i A ) = A )
27 26 fveq2d 
 |-  ( ( A i^i B ) = (/) -> ( vol* ` ( ( A u. B ) i^i A ) ) = ( vol* ` A ) )
28 uncom 
 |-  ( A u. B ) = ( B u. A )
29 28 difeq1i 
 |-  ( ( A u. B ) \ A ) = ( ( B u. A ) \ A )
30 difun2 
 |-  ( ( B u. A ) \ A ) = ( B \ A )
31 29 30 eqtri 
 |-  ( ( A u. B ) \ A ) = ( B \ A )
32 21 eqeq1i 
 |-  ( ( B i^i A ) = (/) <-> ( A i^i B ) = (/) )
33 disj3 
 |-  ( ( B i^i A ) = (/) <-> B = ( B \ A ) )
34 32 33 sylbb1 
 |-  ( ( A i^i B ) = (/) -> B = ( B \ A ) )
35 31 34 eqtr4id 
 |-  ( ( A i^i B ) = (/) -> ( ( A u. B ) \ A ) = B )
36 35 fveq2d 
 |-  ( ( A i^i B ) = (/) -> ( vol* ` ( ( A u. B ) \ A ) ) = ( vol* ` B ) )
37 27 36 oveq12d 
 |-  ( ( A i^i B ) = (/) -> ( ( vol* ` ( ( A u. B ) i^i A ) ) + ( vol* ` ( ( A u. B ) \ A ) ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) )
38 18 37 syl 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` ( ( A u. B ) i^i A ) ) + ( vol* ` ( ( A u. B ) \ A ) ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) )
39 17 38 eqtrd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) )
40 39 ex 
 |-  ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) -> ( ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` ( A u. B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) )
41 mblvol 
 |-  ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )
42 41 eleq1d 
 |-  ( A e. dom vol -> ( ( vol ` A ) e. RR <-> ( vol* ` A ) e. RR ) )
43 mblvol 
 |-  ( B e. dom vol -> ( vol ` B ) = ( vol* ` B ) )
44 43 eleq1d 
 |-  ( B e. dom vol -> ( ( vol ` B ) e. RR <-> ( vol* ` B ) e. RR ) )
45 42 44 bi2anan9 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) <-> ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) )
46 45 3adant3 
 |-  ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) -> ( ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) <-> ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) )
47 unmbl 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A u. B ) e. dom vol )
48 mblvol 
 |-  ( ( A u. B ) e. dom vol -> ( vol ` ( A u. B ) ) = ( vol* ` ( A u. B ) ) )
49 47 48 syl 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( vol ` ( A u. B ) ) = ( vol* ` ( A u. B ) ) )
50 41 43 oveqan12d 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( ( vol ` A ) + ( vol ` B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) )
51 49 50 eqeq12d 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) <-> ( vol* ` ( A u. B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) )
52 51 3adant3 
 |-  ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) -> ( ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) <-> ( vol* ` ( A u. B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) )
53 40 46 52 3imtr4d 
 |-  ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) -> ( ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) -> ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) ) )
54 53 imp 
 |-  ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) )