Metamath Proof Explorer

Theorem mblsplit

Description: The defining property of measurability. (Contributed by Mario Carneiro, 17-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 1 elpw2 
 |-  ( B e. ~P RR <-> B C_ RR )
3 ismbl 
 |-  ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) ) )
4 fveq2 
 |-  ( x = B -> ( vol* ` x ) = ( vol* ` B ) )
5 4 eleq1d 
 |-  ( x = B -> ( ( vol* ` x ) e. RR <-> ( vol* ` B ) e. RR ) )
6 ineq1 
 |-  ( x = B -> ( x i^i A ) = ( B i^i A ) )
7 6 fveq2d 
 |-  ( x = B -> ( vol* ` ( x i^i A ) ) = ( vol* ` ( B i^i A ) ) )
8 difeq1 
 |-  ( x = B -> ( x \ A ) = ( B \ A ) )
9 8 fveq2d 
 |-  ( x = B -> ( vol* ` ( x \ A ) ) = ( vol* ` ( B \ A ) ) )
10 7 9 oveq12d 
 |-  ( x = B -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) )
11 4 10 eqeq12d 
 |-  ( x = B -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <-> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) )
12 5 11 imbi12d 
 |-  ( x = B -> ( ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( ( vol* ` B ) e. RR -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) ) )
13 12 rspccv 
 |-  ( A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) -> ( B e. ~P RR -> ( ( vol* ` B ) e. RR -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) ) )
14 3 13 simplbiim 
 |-  ( A e. dom vol -> ( B e. ~P RR -> ( ( vol* ` B ) e. RR -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) ) )
15 2 14 syl5bir 
 |-  ( A e. dom vol -> ( B C_ RR -> ( ( vol* ` B ) e. RR -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) ) )
16 15 3imp 
 |-  ( ( A e. dom vol /\ B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) )