Metamath Proof Explorer


Theorem volun

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

Ref Expression
Assertion volun ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( 𝐴𝐵 ) ) = ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → 𝐴 ∈ dom vol )
2 mblss ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
3 1 2 syl ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → 𝐴 ⊆ ℝ )
4 simpl2 ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → 𝐵 ∈ dom vol )
5 mblss ( 𝐵 ∈ dom vol → 𝐵 ⊆ ℝ )
6 4 5 syl ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → 𝐵 ⊆ ℝ )
7 3 6 unssd ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴𝐵 ) ⊆ ℝ )
8 readdcl ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ )
9 8 adantl ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ )
10 simprl ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
11 simprr ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ 𝐵 ) ∈ ℝ )
12 ovolun ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )
13 3 10 6 11 12 syl22anc ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )
14 ovollecl ( ( ( 𝐴𝐵 ) ⊆ ℝ ∧ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) ∈ ℝ )
15 7 9 13 14 syl3anc ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) ∈ ℝ )
16 mblsplit ( ( 𝐴 ∈ dom vol ∧ ( 𝐴𝐵 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐴𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴𝐵 ) ) = ( ( vol* ‘ ( ( 𝐴𝐵 ) ∩ 𝐴 ) ) + ( vol* ‘ ( ( 𝐴𝐵 ) ∖ 𝐴 ) ) ) )
17 1 7 15 16 syl3anc ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) = ( ( vol* ‘ ( ( 𝐴𝐵 ) ∩ 𝐴 ) ) + ( vol* ‘ ( ( 𝐴𝐵 ) ∖ 𝐴 ) ) ) )
18 simpl3 ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴𝐵 ) = ∅ )
19 indir ( ( 𝐴𝐵 ) ∩ 𝐴 ) = ( ( 𝐴𝐴 ) ∪ ( 𝐵𝐴 ) )
20 inidm ( 𝐴𝐴 ) = 𝐴
21 incom ( 𝐵𝐴 ) = ( 𝐴𝐵 )
22 20 21 uneq12i ( ( 𝐴𝐴 ) ∪ ( 𝐵𝐴 ) ) = ( 𝐴 ∪ ( 𝐴𝐵 ) )
23 unabs ( 𝐴 ∪ ( 𝐴𝐵 ) ) = 𝐴
24 22 23 eqtri ( ( 𝐴𝐴 ) ∪ ( 𝐵𝐴 ) ) = 𝐴
25 19 24 eqtri ( ( 𝐴𝐵 ) ∩ 𝐴 ) = 𝐴
26 25 a1i ( ( 𝐴𝐵 ) = ∅ → ( ( 𝐴𝐵 ) ∩ 𝐴 ) = 𝐴 )
27 26 fveq2d ( ( 𝐴𝐵 ) = ∅ → ( vol* ‘ ( ( 𝐴𝐵 ) ∩ 𝐴 ) ) = ( vol* ‘ 𝐴 ) )
28 uncom ( 𝐴𝐵 ) = ( 𝐵𝐴 )
29 28 difeq1i ( ( 𝐴𝐵 ) ∖ 𝐴 ) = ( ( 𝐵𝐴 ) ∖ 𝐴 )
30 difun2 ( ( 𝐵𝐴 ) ∖ 𝐴 ) = ( 𝐵𝐴 )
31 29 30 eqtri ( ( 𝐴𝐵 ) ∖ 𝐴 ) = ( 𝐵𝐴 )
32 21 eqeq1i ( ( 𝐵𝐴 ) = ∅ ↔ ( 𝐴𝐵 ) = ∅ )
33 disj3 ( ( 𝐵𝐴 ) = ∅ ↔ 𝐵 = ( 𝐵𝐴 ) )
34 32 33 sylbb1 ( ( 𝐴𝐵 ) = ∅ → 𝐵 = ( 𝐵𝐴 ) )
35 31 34 eqtr4id ( ( 𝐴𝐵 ) = ∅ → ( ( 𝐴𝐵 ) ∖ 𝐴 ) = 𝐵 )
36 35 fveq2d ( ( 𝐴𝐵 ) = ∅ → ( vol* ‘ ( ( 𝐴𝐵 ) ∖ 𝐴 ) ) = ( vol* ‘ 𝐵 ) )
37 27 36 oveq12d ( ( 𝐴𝐵 ) = ∅ → ( ( vol* ‘ ( ( 𝐴𝐵 ) ∩ 𝐴 ) ) + ( vol* ‘ ( ( 𝐴𝐵 ) ∖ 𝐴 ) ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )
38 18 37 syl ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol* ‘ ( ( 𝐴𝐵 ) ∩ 𝐴 ) ) + ( vol* ‘ ( ( 𝐴𝐵 ) ∖ 𝐴 ) ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )
39 17 38 eqtrd ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )
40 39 ex ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) → ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ( 𝐴𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) )
41 mblvol ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) = ( vol* ‘ 𝐴 ) )
42 41 eleq1d ( 𝐴 ∈ dom vol → ( ( vol ‘ 𝐴 ) ∈ ℝ ↔ ( vol* ‘ 𝐴 ) ∈ ℝ ) )
43 mblvol ( 𝐵 ∈ dom vol → ( vol ‘ 𝐵 ) = ( vol* ‘ 𝐵 ) )
44 43 eleq1d ( 𝐵 ∈ dom vol → ( ( vol ‘ 𝐵 ) ∈ ℝ ↔ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
45 42 44 bi2anan9 ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) )
46 45 3adant3 ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) → ( ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) )
47 unmbl ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴𝐵 ) ∈ dom vol )
48 mblvol ( ( 𝐴𝐵 ) ∈ dom vol → ( vol ‘ ( 𝐴𝐵 ) ) = ( vol* ‘ ( 𝐴𝐵 ) ) )
49 47 48 syl ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( vol ‘ ( 𝐴𝐵 ) ) = ( vol* ‘ ( 𝐴𝐵 ) ) )
50 41 43 oveqan12d ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )
51 49 50 eqeq12d ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ( vol ‘ ( 𝐴𝐵 ) ) = ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) ↔ ( vol* ‘ ( 𝐴𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) )
52 51 3adant3 ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) → ( ( vol ‘ ( 𝐴𝐵 ) ) = ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) ↔ ( vol* ‘ ( 𝐴𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) )
53 40 46 52 3imtr4d ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) → ( ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) → ( vol ‘ ( 𝐴𝐵 ) ) = ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) ) )
54 53 imp ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴𝐵 ) = ∅ ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( 𝐴𝐵 ) ) = ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) )