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