Theorem volinun

Description: Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015)

	Ref	Expression
Assertion	volinun	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) = ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		inundif	⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
2	1	fveq2i	⊢ ( vol ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( vol ‘ 𝐴 )
3		inmbl	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∩ 𝐵 ) ∈ dom vol )
4	3	adantr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴 ∩ 𝐵 ) ∈ dom vol )
5		difmbl	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∖ 𝐵 ) ∈ dom vol )
6	5	adantr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴 ∖ 𝐵 ) ∈ dom vol )
7		indifcom	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐴 ∩ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐵 ) )
8		difin0	⊢ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐵 ) = ∅
9	8	ineq2i	⊢ ( 𝐴 ∩ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐵 ) ) = ( 𝐴 ∩ ∅ )
10		in0	⊢ ( 𝐴 ∩ ∅ ) = ∅
11	9 10	eqtri	⊢ ( 𝐴 ∩ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐵 ) ) = ∅
12	7 11	eqtri	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
13	12	a1i	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ )
14		mblvol	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ dom vol → ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) = ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) )
15	4 14	syl	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) = ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) )
16		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
17	16	a1i	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 )
18		mblss	⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
19	18	ad2antrr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → 𝐴 ⊆ ℝ )
20		mblvol	⊢ ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) = ( vol* ‘ 𝐴 ) )
21	20	ad2antrr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ 𝐴 ) = ( vol* ‘ 𝐴 ) )
22		simprl	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ 𝐴 ) ∈ ℝ )
23	21 22	eqeltrrd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
24		ovolsscl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ )
25	17 19 23 24	syl3anc	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ )
26	15 25	eqeltrd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ )
27		mblvol	⊢ ( ( 𝐴 ∖ 𝐵 ) ∈ dom vol → ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) = ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) )
28	6 27	syl	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) = ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) )
29		difssd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 )
30		ovolsscl	⊢ ( ( ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ )
31	29 19 23 30	syl3anc	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ )
32	28 31	eqeltrd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ )
33		volun	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) ∈ dom vol ∧ ( 𝐴 ∖ 𝐵 ) ∈ dom vol ∧ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ ) ∧ ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℝ ∧ ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
34	4 6 13 26 32 33	syl32anc	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
35	2 34	syl5eqr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ 𝐴 ) = ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
36	35	oveq1d	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) = ( ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ) + ( vol ‘ 𝐵 ) ) )
37	26	recnd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ℂ )
38	32	recnd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℂ )
39		simprr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ 𝐵 ) ∈ ℝ )
40	39	recnd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ 𝐵 ) ∈ ℂ )
41	37 38 40	addassd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ) + ( vol ‘ 𝐵 ) ) = ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) + ( vol ‘ 𝐵 ) ) ) )
42		undif1	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 )
43	42	fveq2i	⊢ ( vol ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ) = ( vol ‘ ( 𝐴 ∪ 𝐵 ) )
44		simplr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → 𝐵 ∈ dom vol )
45		incom	⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) )
46		disjdif	⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
47	45 46	eqtri	⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅
48	47	a1i	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅ )
49		volun	⊢ ( ( ( ( 𝐴 ∖ 𝐵 ) ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅ ) ∧ ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ) = ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) + ( vol ‘ 𝐵 ) ) )
50	6 44 48 32 39 49	syl32anc	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ) = ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) + ( vol ‘ 𝐵 ) ) )
51	43 50	syl5reqr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) + ( vol ‘ 𝐵 ) ) = ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) )
52	51	oveq2d	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) + ( vol ‘ 𝐵 ) ) ) = ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
53	36 41 52	3eqtrd	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) = ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) ) )