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 ) ) ) )