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 syl5eqr 
 |-  ( ( ( 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 undif1 
 |-  ( ( A \ B ) u. B ) = ( A u. B )
43 42 fveq2i 
 |-  ( vol ` ( ( A \ B ) u. B ) ) = ( vol ` ( A u. B ) )
44 simplr 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> B e. dom vol )
45 incom 
 |-  ( ( A \ B ) i^i B ) = ( B i^i ( A \ B ) )
46 disjdif 
 |-  ( B i^i ( A \ B ) ) = (/)
47 45 46 eqtri 
 |-  ( ( A \ B ) i^i B ) = (/)
48 47 a1i 
 |-  ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( ( A \ B ) i^i B ) = (/) )
49 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 ) ) )
50 6 44 48 32 39 49 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 ) ) )
51 43 50 syl5reqr 
 |-  ( ( ( 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 ) ) )
52 51 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 ) ) ) )
53 36 41 52 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 ) ) ) )