Metamath Proof Explorer

Theorem volinun

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

Ref Expression
Assertion volinun 
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( ( vol ` A ) + ( vol ` B ) ) = ( ( vol ` ( A i^i B ) ) + ( vol ` ( A u. B ) ) ) )

Proof

Step Hyp Ref Expression
1 inundif 
 |-  ( ( A i^i B ) u. ( A \ B ) ) = A
2 1 fveq2i 
 |-  ( vol ` ( ( A i^i B ) u. ( A \ B ) ) ) = ( vol ` A )
3 inmbl 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A i^i B ) e. dom vol )
4 3 adantr 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( A i^i B ) e. dom vol )
5 difmbl 
 |-  ( ( A e. dom vol /\ B e. dom vol ) -> ( A \ B ) e. dom vol )
6 5 adantr 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( A \ B ) e. dom vol )
7 indifcom 
 |-  ( ( A i^i B ) i^i ( A \ B ) ) = ( A i^i ( ( A i^i B ) \ B ) )
8 difin0 
 |-  ( ( A i^i B ) \ B ) = (/)
9 8 ineq2i 
 |-  ( A i^i ( ( A i^i B ) \ B ) ) = ( A i^i (/) )
10 in0 
 |-  ( A i^i (/) ) = (/)
11 9 10 eqtri 
 |-  ( A i^i ( ( A i^i B ) \ B ) ) = (/)
12 7 11 eqtri 
 |-  ( ( A i^i B ) i^i ( A \ B ) ) = (/)
13 12 a1i 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( ( A i^i B ) i^i ( A \ B ) ) = (/) )
14 mblvol 
 |-  ( ( A i^i B ) e. dom vol -> ( vol ` ( A i^i B ) ) = ( vol* ` ( A i^i B ) ) )
15 4 14 syl 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( A i^i B ) ) = ( vol* ` ( A i^i B ) ) )
16 inss1 
 |-  ( A i^i B ) C_ A
17 16 a1i 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( A i^i B ) C_ A )
18 mblss 
 |-  ( A e. dom vol -> A C_ RR )
19 18 ad2antrr 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> A C_ RR )
20 mblvol 
 |-  ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )
21 20 ad2antrr 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` A ) = ( vol* ` A ) )
22 simprl 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` A ) e. RR )
23 21 22 eqeltrrd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol* ` A ) e. RR )
24 ovolsscl 
 |-  ( ( ( A i^i B ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A i^i B ) ) e. RR )
25 17 19 23 24 syl3anc 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol* ` ( A i^i B ) ) e. RR )
26 15 25 eqeltrd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( A i^i B ) ) e. RR )
27 mblvol 
 |-  ( ( A \ B ) e. dom vol -> ( vol ` ( A \ B ) ) = ( vol* ` ( A \ B ) ) )
28 6 27 syl 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( A \ B ) ) = ( vol* ` ( A \ B ) ) )
29 difssd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( A \ B ) C_ A )
30 ovolsscl 
 |-  ( ( ( A \ B ) C_ A /\ A C_ RR /\ ( vol* ` A ) e. RR ) -> ( vol* ` ( A \ B ) ) e. RR )
31 29 19 23 30 syl3anc 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol* ` ( A \ B ) ) e. RR )
32 28 31 eqeltrd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( A \ B ) ) e. RR )
33 volun 
 |-  ( ( ( ( A i^i B ) e. dom vol /\ ( A \ B ) e. dom vol /\ ( ( A i^i B ) i^i ( A \ B ) ) = (/) ) /\ ( ( vol ` ( A i^i B ) ) e. RR /\ ( vol ` ( A \ B ) ) e. RR ) ) -> ( vol ` ( ( A i^i B ) u. ( A \ B ) ) ) = ( ( vol ` ( A i^i B ) ) + ( vol ` ( A \ B ) ) ) )
34 4 6 13 26 32 33 syl32anc 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( ( A i^i B ) u. ( A \ B ) ) ) = ( ( vol ` ( A i^i B ) ) + ( vol ` ( A \ B ) ) ) )
35 2 34 eqtr3id 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` A ) = ( ( vol ` ( A i^i B ) ) + ( vol ` ( A \ B ) ) ) )
36 35 oveq1d 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( ( vol ` A ) + ( vol ` B ) ) = ( ( ( vol ` ( A i^i B ) ) + ( vol ` ( A \ B ) ) ) + ( vol ` B ) ) )
37 26 recnd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( A i^i B ) ) e. CC )
38 32 recnd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( A \ B ) ) e. CC )
39 simprr 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` B ) e. RR )
40 39 recnd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` B ) e. CC )
41 37 38 40 addassd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( ( ( vol ` ( A i^i B ) ) + ( vol ` ( A \ B ) ) ) + ( vol ` B ) ) = ( ( vol ` ( A i^i B ) ) + ( ( vol ` ( A \ B ) ) + ( vol ` B ) ) ) )
42 simplr 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> B e. dom vol )
43 disjdifr 
 |-  ( ( A \ B ) i^i B ) = (/)
44 43 a1i 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( ( A \ B ) i^i B ) = (/) )
45 volun 
 |-  ( ( ( ( A \ B ) e. dom vol /\ B e. dom vol /\ ( ( A \ B ) i^i B ) = (/) ) /\ ( ( vol ` ( A \ B ) ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( ( A \ B ) u. B ) ) = ( ( vol ` ( A \ B ) ) + ( vol ` B ) ) )
46 6 42 44 32 39 45 syl32anc 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( ( A \ B ) u. B ) ) = ( ( vol ` ( A \ B ) ) + ( vol ` B ) ) )
47 undif1 
 |-  ( ( A \ B ) u. B ) = ( A u. B )
48 47 fveq2i 
 |-  ( vol ` ( ( A \ B ) u. B ) ) = ( vol ` ( A u. B ) )
49 46 48 eqtr3di 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( ( vol ` ( A \ B ) ) + ( vol ` B ) ) = ( vol ` ( A u. B ) ) )
50 49 oveq2d 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( ( vol ` ( A i^i B ) ) + ( ( vol ` ( A \ B ) ) + ( vol ` B ) ) ) = ( ( vol ` ( A i^i B ) ) + ( vol ` ( A u. B ) ) ) )
51 36 41 50 3eqtrd 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( ( vol ` A ) + ( vol ` B ) ) = ( ( vol ` ( A i^i B ) ) + ( vol ` ( A u. B ) ) ) )