# Metamath Proof Explorer

## Theorem volun

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

Ref Expression
Assertion volun ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left(vol\left({A}\right)\in ℝ\wedge vol\left({B}\right)\in ℝ\right)\right)\to vol\left({A}\cup {B}\right)=vol\left({A}\right)+vol\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 simpl1 ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {A}\in \mathrm{dom}vol$
2 mblss ${⊢}{A}\in \mathrm{dom}vol\to {A}\subseteq ℝ$
3 1 2 syl ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {A}\subseteq ℝ$
4 simpl2 ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {B}\in \mathrm{dom}vol$
5 mblss ${⊢}{B}\in \mathrm{dom}vol\to {B}\subseteq ℝ$
6 4 5 syl ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {B}\subseteq ℝ$
7 3 6 unssd ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {A}\cup {B}\subseteq ℝ$
8 readdcl ${⊢}\left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\to {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\in ℝ$
9 8 adantl ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\in ℝ$
10 simprl ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\right)\in ℝ$
11 simprr ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({B}\right)\in ℝ$
12 ovolun ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)$
13 3 10 6 11 12 syl22anc ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)$
14 ovollecl ${⊢}\left({A}\cup {B}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\in ℝ\wedge {vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\right)\to {vol}^{*}\left({A}\cup {B}\right)\in ℝ$
15 7 9 13 14 syl3anc ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\cup {B}\right)\in ℝ$
16 mblsplit ${⊢}\left({A}\in \mathrm{dom}vol\wedge {A}\cup {B}\subseteq ℝ\wedge {vol}^{*}\left({A}\cup {B}\right)\in ℝ\right)\to {vol}^{*}\left({A}\cup {B}\right)={vol}^{*}\left(\left({A}\cup {B}\right)\cap {A}\right)+{vol}^{*}\left(\left({A}\cup {B}\right)\setminus {A}\right)$
17 1 7 15 16 syl3anc ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\cup {B}\right)={vol}^{*}\left(\left({A}\cup {B}\right)\cap {A}\right)+{vol}^{*}\left(\left({A}\cup {B}\right)\setminus {A}\right)$
18 simpl3 ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {A}\cap {B}=\varnothing$
19 indir ${⊢}\left({A}\cup {B}\right)\cap {A}=\left({A}\cap {A}\right)\cup \left({B}\cap {A}\right)$
20 inidm ${⊢}{A}\cap {A}={A}$
21 incom ${⊢}{B}\cap {A}={A}\cap {B}$
22 20 21 uneq12i ${⊢}\left({A}\cap {A}\right)\cup \left({B}\cap {A}\right)={A}\cup \left({A}\cap {B}\right)$
23 unabs ${⊢}{A}\cup \left({A}\cap {B}\right)={A}$
24 22 23 eqtri ${⊢}\left({A}\cap {A}\right)\cup \left({B}\cap {A}\right)={A}$
25 19 24 eqtri ${⊢}\left({A}\cup {B}\right)\cap {A}={A}$
26 25 a1i ${⊢}{A}\cap {B}=\varnothing \to \left({A}\cup {B}\right)\cap {A}={A}$
27 26 fveq2d ${⊢}{A}\cap {B}=\varnothing \to {vol}^{*}\left(\left({A}\cup {B}\right)\cap {A}\right)={vol}^{*}\left({A}\right)$
28 uncom ${⊢}{A}\cup {B}={B}\cup {A}$
29 28 difeq1i ${⊢}\left({A}\cup {B}\right)\setminus {A}=\left({B}\cup {A}\right)\setminus {A}$
30 difun2 ${⊢}\left({B}\cup {A}\right)\setminus {A}={B}\setminus {A}$
31 29 30 eqtri ${⊢}\left({A}\cup {B}\right)\setminus {A}={B}\setminus {A}$
32 21 eqeq1i ${⊢}{B}\cap {A}=\varnothing ↔{A}\cap {B}=\varnothing$
33 disj3 ${⊢}{B}\cap {A}=\varnothing ↔{B}={B}\setminus {A}$
34 32 33 sylbb1 ${⊢}{A}\cap {B}=\varnothing \to {B}={B}\setminus {A}$
35 31 34 eqtr4id ${⊢}{A}\cap {B}=\varnothing \to \left({A}\cup {B}\right)\setminus {A}={B}$
36 35 fveq2d ${⊢}{A}\cap {B}=\varnothing \to {vol}^{*}\left(\left({A}\cup {B}\right)\setminus {A}\right)={vol}^{*}\left({B}\right)$
37 27 36 oveq12d ${⊢}{A}\cap {B}=\varnothing \to {vol}^{*}\left(\left({A}\cup {B}\right)\cap {A}\right)+{vol}^{*}\left(\left({A}\cup {B}\right)\setminus {A}\right)={vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)$
38 18 37 syl ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left(\left({A}\cup {B}\right)\cap {A}\right)+{vol}^{*}\left(\left({A}\cup {B}\right)\setminus {A}\right)={vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)$
39 17 38 eqtrd ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\cup {B}\right)={vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)$
40 39 ex ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\to \left(\left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\to {vol}^{*}\left({A}\cup {B}\right)={vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\right)$
41 mblvol ${⊢}{A}\in \mathrm{dom}vol\to vol\left({A}\right)={vol}^{*}\left({A}\right)$
42 41 eleq1d ${⊢}{A}\in \mathrm{dom}vol\to \left(vol\left({A}\right)\in ℝ↔{vol}^{*}\left({A}\right)\in ℝ\right)$
43 mblvol ${⊢}{B}\in \mathrm{dom}vol\to vol\left({B}\right)={vol}^{*}\left({B}\right)$
44 43 eleq1d ${⊢}{B}\in \mathrm{dom}vol\to \left(vol\left({B}\right)\in ℝ↔{vol}^{*}\left({B}\right)\in ℝ\right)$
45 42 44 bi2anan9 ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to \left(\left(vol\left({A}\right)\in ℝ\wedge vol\left({B}\right)\in ℝ\right)↔\left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)$
46 45 3adant3 ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\to \left(\left(vol\left({A}\right)\in ℝ\wedge vol\left({B}\right)\in ℝ\right)↔\left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)$
47 unmbl ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to {A}\cup {B}\in \mathrm{dom}vol$
48 mblvol ${⊢}{A}\cup {B}\in \mathrm{dom}vol\to vol\left({A}\cup {B}\right)={vol}^{*}\left({A}\cup {B}\right)$
49 47 48 syl ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to vol\left({A}\cup {B}\right)={vol}^{*}\left({A}\cup {B}\right)$
50 41 43 oveqan12d ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to vol\left({A}\right)+vol\left({B}\right)={vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)$
51 49 50 eqeq12d ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to \left(vol\left({A}\cup {B}\right)=vol\left({A}\right)+vol\left({B}\right)↔{vol}^{*}\left({A}\cup {B}\right)={vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\right)$
52 51 3adant3 ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\to \left(vol\left({A}\cup {B}\right)=vol\left({A}\right)+vol\left({B}\right)↔{vol}^{*}\left({A}\cup {B}\right)={vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\right)$
53 40 46 52 3imtr4d ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\to \left(\left(vol\left({A}\right)\in ℝ\wedge vol\left({B}\right)\in ℝ\right)\to vol\left({A}\cup {B}\right)=vol\left({A}\right)+vol\left({B}\right)\right)$
54 53 imp ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\wedge {A}\cap {B}=\varnothing \right)\wedge \left(vol\left({A}\right)\in ℝ\wedge vol\left({B}\right)\in ℝ\right)\right)\to vol\left({A}\cup {B}\right)=vol\left({A}\right)+vol\left({B}\right)$