Metamath Proof Explorer

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 eqtr3id ⊢ ( ( ( 𝐴 ∈ 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 simplr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → 𝐵 ∈ dom vol )
43 disjdifr ⊢ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅
44 43 a1i ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅ )
45 volun ⊢ ( ( ( ( 𝐴 ∖ 𝐵 ) ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( ( 𝐴 ∖ 𝐵 ) ∩ 𝐵 ) = ∅ ) ∧ ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ) = ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) + ( vol ‘ 𝐵 ) ) )
46 6 42 44 32 39 45 syl32anc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ) = ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) + ( vol ‘ 𝐵 ) ) )
47 undif1 ⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = ( 𝐴 ∪ 𝐵 )
48 47 fveq2i ⊢ ( vol ‘ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ) = ( vol ‘ ( 𝐴 ∪ 𝐵 ) )
49 46 48 eqtr3di ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) + ( vol ‘ 𝐵 ) ) = ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) )
50 49 oveq2d ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( ( vol ‘ ( 𝐴 ∖ 𝐵 ) ) + ( vol ‘ 𝐵 ) ) ) = ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
51 36 41 50 3eqtrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) = ( ( vol ‘ ( 𝐴 ∩ 𝐵 ) ) + ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) ) )