Metamath Proof Explorer

Theorem shftmbl

Description: A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014)

Ref Expression
Assertion shftmbl 
|- ( ( A e. dom vol /\ B e. RR ) -> { x e. RR | ( x - B ) e. A } e. dom vol )

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { x e. RR | ( x - B ) e. A } C_ RR
2 1 a1i 
 |-  ( ( A e. dom vol /\ B e. RR ) -> { x e. RR | ( x - B ) e. A } C_ RR )
3 elpwi 
 |-  ( y e. ~P RR -> y C_ RR )
4 simpll 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> A e. dom vol )
5 ssrab2 
 |-  { z e. RR | ( z - -u B ) e. y } C_ RR
6 5 a1i 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> { z e. RR | ( z - -u B ) e. y } C_ RR )
7 simprl 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> y C_ RR )
8 simplr 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> B e. RR )
9 8 renegcld 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> -u B e. RR )
10 eqidd 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> { z e. RR | ( z - -u B ) e. y } = { z e. RR | ( z - -u B ) e. y } )
11 7 9 10 ovolshft 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( vol* ` y ) = ( vol* ` { z e. RR | ( z - -u B ) e. y } ) )
12 simprr 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( vol* ` y ) e. RR )
13 11 12 eqeltrrd 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( vol* ` { z e. RR | ( z - -u B ) e. y } ) e. RR )
14 mblsplit 
 |-  ( ( A e. dom vol /\ { z e. RR | ( z - -u B ) e. y } C_ RR /\ ( vol* ` { z e. RR | ( z - -u B ) e. y } ) e. RR ) -> ( vol* ` { z e. RR | ( z - -u B ) e. y } ) = ( ( vol* ` ( { z e. RR | ( z - -u B ) e. y } i^i A ) ) + ( vol* ` ( { z e. RR | ( z - -u B ) e. y } \ A ) ) ) )
15 4 6 13 14 syl3anc 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( vol* ` { z e. RR | ( z - -u B ) e. y } ) = ( ( vol* ` ( { z e. RR | ( z - -u B ) e. y } i^i A ) ) + ( vol* ` ( { z e. RR | ( z - -u B ) e. y } \ A ) ) ) )
16 inss1 
 |-  ( y i^i { x e. RR | ( x - B ) e. A } ) C_ y
17 16 7 sstrid 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( y i^i { x e. RR | ( x - B ) e. A } ) C_ RR )
18 mblss 
 |-  ( A e. dom vol -> A C_ RR )
19 4 18 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> A C_ RR )
20 eqidd 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> { x e. RR | ( x - B ) e. A } = { x e. RR | ( x - B ) e. A } )
21 19 8 20 shft2rab 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> A = { z e. RR | ( z - -u B ) e. { x e. RR | ( x - B ) e. A } } )
22 21 ineq2d 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( { z e. RR | ( z - -u B ) e. y } i^i A ) = ( { z e. RR | ( z - -u B ) e. y } i^i { z e. RR | ( z - -u B ) e. { x e. RR | ( x - B ) e. A } } ) )
23 inrab 
 |-  ( { z e. RR | ( z - -u B ) e. y } i^i { z e. RR | ( z - -u B ) e. { x e. RR | ( x - B ) e. A } } ) = { z e. RR | ( ( z - -u B ) e. y /\ ( z - -u B ) e. { x e. RR | ( x - B ) e. A } ) }
24 elin 
 |-  ( ( z - -u B ) e. ( y i^i { x e. RR | ( x - B ) e. A } ) <-> ( ( z - -u B ) e. y /\ ( z - -u B ) e. { x e. RR | ( x - B ) e. A } ) )
25 24 rabbii 
 |-  { z e. RR | ( z - -u B ) e. ( y i^i { x e. RR | ( x - B ) e. A } ) } = { z e. RR | ( ( z - -u B ) e. y /\ ( z - -u B ) e. { x e. RR | ( x - B ) e. A } ) }
26 23 25 eqtr4i 
 |-  ( { z e. RR | ( z - -u B ) e. y } i^i { z e. RR | ( z - -u B ) e. { x e. RR | ( x - B ) e. A } } ) = { z e. RR | ( z - -u B ) e. ( y i^i { x e. RR | ( x - B ) e. A } ) }
27 22 26 eqtrdi 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( { z e. RR | ( z - -u B ) e. y } i^i A ) = { z e. RR | ( z - -u B ) e. ( y i^i { x e. RR | ( x - B ) e. A } ) } )
28 17 9 27 ovolshft 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( vol* ` ( y i^i { x e. RR | ( x - B ) e. A } ) ) = ( vol* ` ( { z e. RR | ( z - -u B ) e. y } i^i A ) ) )
29 7 ssdifssd 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( y \ { x e. RR | ( x - B ) e. A } ) C_ RR )
30 21 difeq2d 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( { z e. RR | ( z - -u B ) e. y } \ A ) = ( { z e. RR | ( z - -u B ) e. y } \ { z e. RR | ( z - -u B ) e. { x e. RR | ( x - B ) e. A } } ) )
31 difrab 
 |-  ( { z e. RR | ( z - -u B ) e. y } \ { z e. RR | ( z - -u B ) e. { x e. RR | ( x - B ) e. A } } ) = { z e. RR | ( ( z - -u B ) e. y /\ -. ( z - -u B ) e. { x e. RR | ( x - B ) e. A } ) }
32 eldif 
 |-  ( ( z - -u B ) e. ( y \ { x e. RR | ( x - B ) e. A } ) <-> ( ( z - -u B ) e. y /\ -. ( z - -u B ) e. { x e. RR | ( x - B ) e. A } ) )
33 32 rabbii 
 |-  { z e. RR | ( z - -u B ) e. ( y \ { x e. RR | ( x - B ) e. A } ) } = { z e. RR | ( ( z - -u B ) e. y /\ -. ( z - -u B ) e. { x e. RR | ( x - B ) e. A } ) }
34 31 33 eqtr4i 
 |-  ( { z e. RR | ( z - -u B ) e. y } \ { z e. RR | ( z - -u B ) e. { x e. RR | ( x - B ) e. A } } ) = { z e. RR | ( z - -u B ) e. ( y \ { x e. RR | ( x - B ) e. A } ) }
35 30 34 eqtrdi 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( { z e. RR | ( z - -u B ) e. y } \ A ) = { z e. RR | ( z - -u B ) e. ( y \ { x e. RR | ( x - B ) e. A } ) } )
36 29 9 35 ovolshft 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( vol* ` ( y \ { x e. RR | ( x - B ) e. A } ) ) = ( vol* ` ( { z e. RR | ( z - -u B ) e. y } \ A ) ) )
37 28 36 oveq12d 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( ( vol* ` ( y i^i { x e. RR | ( x - B ) e. A } ) ) + ( vol* ` ( y \ { x e. RR | ( x - B ) e. A } ) ) ) = ( ( vol* ` ( { z e. RR | ( z - -u B ) e. y } i^i A ) ) + ( vol* ` ( { z e. RR | ( z - -u B ) e. y } \ A ) ) ) )
38 15 11 37 3eqtr4d 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ ( y C_ RR /\ ( vol* ` y ) e. RR ) ) -> ( vol* ` y ) = ( ( vol* ` ( y i^i { x e. RR | ( x - B ) e. A } ) ) + ( vol* ` ( y \ { x e. RR | ( x - B ) e. A } ) ) ) )
39 38 expr 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ y C_ RR ) -> ( ( vol* ` y ) e. RR -> ( vol* ` y ) = ( ( vol* ` ( y i^i { x e. RR | ( x - B ) e. A } ) ) + ( vol* ` ( y \ { x e. RR | ( x - B ) e. A } ) ) ) ) )
40 3 39 sylan2 
 |-  ( ( ( A e. dom vol /\ B e. RR ) /\ y e. ~P RR ) -> ( ( vol* ` y ) e. RR -> ( vol* ` y ) = ( ( vol* ` ( y i^i { x e. RR | ( x - B ) e. A } ) ) + ( vol* ` ( y \ { x e. RR | ( x - B ) e. A } ) ) ) ) )
41 40 ralrimiva 
 |-  ( ( A e. dom vol /\ B e. RR ) -> A. y e. ~P RR ( ( vol* ` y ) e. RR -> ( vol* ` y ) = ( ( vol* ` ( y i^i { x e. RR | ( x - B ) e. A } ) ) + ( vol* ` ( y \ { x e. RR | ( x - B ) e. A } ) ) ) ) )
42 ismbl 
 |-  ( { x e. RR | ( x - B ) e. A } e. dom vol <-> ( { x e. RR | ( x - B ) e. A } C_ RR /\ A. y e. ~P RR ( ( vol* ` y ) e. RR -> ( vol* ` y ) = ( ( vol* ` ( y i^i { x e. RR | ( x - B ) e. A } ) ) + ( vol* ` ( y \ { x e. RR | ( x - B ) e. A } ) ) ) ) ) )
43 2 41 42 sylanbrc 
 |-  ( ( A e. dom vol /\ B e. RR ) -> { x e. RR | ( x - B ) e. A } e. dom vol )