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 dom vol B dom vol A B = vol A vol B vol A B = vol A + vol B

Proof

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