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 ) ) )