Theorem volun 22484

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

Assertion

Ref	Expression
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 of Theorem volun

Step	Hyp	Ref	Expression
1		simpl1 1008	. . . . . 6 |- ( ( ( 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 22471	. . . . . . . 8 |- ( A e. dom vol -> A C_ RR )
3	1, 2	syl 17	. . . . . . 7 |- ( ( ( 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 1009	. . . . . . . 8 |- ( ( ( 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 22471	. . . . . . . 8 |- ( B e. dom vol -> B C_ RR )
6	4, 5	syl 17	. . . . . . 7 |- ( ( ( 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 3642	. . . . . 6 |- ( ( ( 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 9622	. . . . . . . 8 |- ( ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR )
9	8	adantl 467	. . . . . . 7 |- ( ( ( 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 762	. . . . . . . 8 |- ( ( ( 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 764	. . . . . . . 8 |- ( ( ( 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 22438	. . . . . . . 8 |- ( ( ( 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 1265	. . . . . . 7 |- ( ( ( 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 22422	. . . . . . 7 |- ( ( ( 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 1264	. . . . . 6 |- ( ( ( 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 22472	. . . . . 6 |- ( ( 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 1264	. . . . 5 |- ( ( ( 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 1010	. . . . . 6 |- ( ( ( 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 3721	. . . . . . . . . 10 |- ( ( A u. B ) i^i A ) = ( ( A i^i A ) u. ( B i^i A ) )
20		inidm 3671	. . . . . . . . . . . 12 |- ( A i^i A ) = A
21		incom 3655	. . . . . . . . . . . 12 |- ( B i^i A ) = ( A i^i B )
22	20, 21	uneq12i 3618	. . . . . . . . . . 11 |- ( ( A i^i A ) u. ( B i^i A ) ) = ( A u. ( A i^i B ) )
23		unabs 3703	. . . . . . . . . . 11 |- ( A u. ( A i^i B ) ) = A
24	22, 23	eqtri 2451	. . . . . . . . . 10 |- ( ( A i^i A ) u. ( B i^i A ) ) = A
25	19, 24	eqtri 2451	. . . . . . . . 9 |- ( ( A u. B ) i^i A ) = A
26	25	a1i 11	. . . . . . . 8 |- ( ( A i^i B ) = (/) -> ( ( A u. B ) i^i A ) = A )
27	26	fveq2d 5881	. . . . . . 7 |- ( ( A i^i B ) = (/) -> ( vol* ` ( ( A u. B ) i^i A ) ) = ( vol* ` A ) )
28	21	eqeq1i 2429	. . . . . . . . . . 11 |- ( ( B i^i A ) = (/) <-> ( A i^i B ) = (/) )
29		disj3 3837	. . . . . . . . . . 11 |- ( ( B i^i A ) = (/) <-> B = ( B \ A ) )
30	28, 29	bitr3i 254	. . . . . . . . . 10 |- ( ( A i^i B ) = (/) <-> B = ( B \ A ) )
31	30	biimpi 197	. . . . . . . . 9 |- ( ( A i^i B ) = (/) -> B = ( B \ A ) )
32		uncom 3610	. . . . . . . . . . 11 |- ( A u. B ) = ( B u. A )
33	32	difeq1i 3579	. . . . . . . . . 10 |- ( ( A u. B ) \ A ) = ( ( B u. A ) \ A )
34		difun2 3875	. . . . . . . . . 10 |- ( ( B u. A ) \ A ) = ( B \ A )
35	33, 34	eqtri 2451	. . . . . . . . 9 |- ( ( A u. B ) \ A ) = ( B \ A )
36	31, 35	syl6reqr 2482	. . . . . . . 8 |- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ A ) = B )
37	36	fveq2d 5881	. . . . . . 7 |- ( ( A i^i B ) = (/) -> ( vol* ` ( ( A u. B ) \ A ) ) = ( vol* ` B ) )
38	27, 37	oveq12d 6319	. . . . . 6 |- ( ( A i^i B ) = (/) -> ( ( vol* ` ( ( A u. B ) i^i A ) ) + ( vol* ` ( ( A u. B ) \ A ) ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) )
39	18, 38	syl 17	. . . . 5 |- ( ( ( 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 ) ) )
40	17, 39	eqtrd 2463	. . . 4 |- ( ( ( 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	40	ex 435	. . 3 |- ( ( 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 ) ) ) )
42		mblvol 22470	. . . . . 6 |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )
43	42	eleq1d 2491	. . . . 5 |- ( A e. dom vol -> ( ( vol ` A ) e. RR <-> ( vol* ` A ) e. RR ) )
44		mblvol 22470	. . . . . 6 |- ( B e. dom vol -> ( vol ` B ) = ( vol* ` B ) )
45	44	eleq1d 2491	. . . . 5 |- ( B e. dom vol -> ( ( vol ` B ) e. RR <-> ( vol* ` B ) e. RR ) )
46	43, 45	bi2anan9 881	. . . 4 |- ( ( A e. dom vol /\ B e. dom vol ) -> ( ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) <-> ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) )
47	46	3adant3 1025	. . 3 |- ( ( 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 ) ) )
48		unmbl 22477	. . . . . 6 |- ( ( A e. dom vol /\ B e. dom vol ) -> ( A u. B ) e. dom vol )
49		mblvol 22470	. . . . . 6 |- ( ( A u. B ) e. dom vol -> ( vol ` ( A u. B ) ) = ( vol* ` ( A u. B ) ) )
50	48, 49	syl 17	. . . . 5 |- ( ( A e. dom vol /\ B e. dom vol ) -> ( vol ` ( A u. B ) ) = ( vol* ` ( A u. B ) ) )
51	42, 44	oveqan12d 6320	. . . . 5 |- ( ( A e. dom vol /\ B e. dom vol ) -> ( ( vol ` A ) + ( vol ` B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) )
52	50, 51	eqeq12d 2444	. . . 4 |- ( ( A e. dom vol /\ B e. dom vol ) -> ( ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) <-> ( vol* ` ( A u. B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) )
53	52	3adant3 1025	. . 3 |- ( ( 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 ) ) ) )
54	41, 47, 53	3imtr4d 271	. 2 |- ( ( 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 ) ) ) )
55	54	imp 430	1 |- ( ( ( 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 ) ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1868   \ cdif 3433   u. cun 3434   i^i cin 3435   C_ wss 3436   (/)c0 3761   class class class wbr 4420   dom cdm 4849   ` cfv 5597  (class class class)co 6301   RRcr 9538   + caddc 9542   <_ cle 9676   vol*covol 22399   volcvol 22401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-er 7367  df-map 7478  df-en 7574  df-dom 7575  df-sdom 7576  df-sup 7958  df-inf 7959  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-q 11265  df-rp 11303  df-ioo 11639  df-ico 11641  df-icc 11642  df-fz 11785  df-fl 12027  df-seq 12213  df-exp 12272  df-cj 13150  df-re 13151  df-im 13152  df-sqrt 13286  df-abs 13287  df-ovol 22402  df-vol 22404

This theorem is referenced by:  volinun  22485  volfiniun  22486  volsup  22495  ovolioo  22507  ismblfin  31894  volioc  37668  volico  38137