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 ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) → { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ∈ dom vol )

Proof

Step Hyp Ref Expression
1 ssrab2 { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ⊆ ℝ
2 1 a1i ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) → { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ⊆ ℝ )
3 elpwi ( 𝑦 ∈ 𝒫 ℝ → 𝑦 ⊆ ℝ )
4 simpll ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → 𝐴 ∈ dom vol )
5 ssrab2 { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ⊆ ℝ
6 5 a1i ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ⊆ ℝ )
7 simprl ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → 𝑦 ⊆ ℝ )
8 simplr ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → 𝐵 ∈ ℝ )
9 8 renegcld ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → - 𝐵 ∈ ℝ )
10 eqidd ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } = { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } )
11 7 9 10 ovolshft ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( vol* ‘ 𝑦 ) = ( vol* ‘ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ) )
12 simprr ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( vol* ‘ 𝑦 ) ∈ ℝ )
13 11 12 eqeltrrd ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( vol* ‘ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ) ∈ ℝ )
14 mblsplit ( ( 𝐴 ∈ dom vol ∧ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ⊆ ℝ ∧ ( vol* ‘ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ) ∈ ℝ ) → ( vol* ‘ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ) = ( ( vol* ‘ ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∩ 𝐴 ) ) + ( vol* ‘ ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∖ 𝐴 ) ) ) )
15 4 6 13 14 syl3anc ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( vol* ‘ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ) = ( ( vol* ‘ ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∩ 𝐴 ) ) + ( vol* ‘ ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∖ 𝐴 ) ) ) )
16 inss1 ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ⊆ 𝑦
17 16 7 sstrid ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ⊆ ℝ )
18 mblss ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
19 4 18 syl ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → 𝐴 ⊆ ℝ )
20 eqidd ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } = { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } )
21 19 8 20 shft2rab ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → 𝐴 = { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } } )
22 21 ineq2d ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∩ 𝐴 ) = ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∩ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } } ) )
23 inrab ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∩ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } } ) = { 𝑧 ∈ ℝ ∣ ( ( 𝑧 − - 𝐵 ) ∈ 𝑦 ∧ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) }
24 elin ( ( 𝑧 − - 𝐵 ) ∈ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ↔ ( ( 𝑧 − - 𝐵 ) ∈ 𝑦 ∧ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) )
25 24 rabbii { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) } = { 𝑧 ∈ ℝ ∣ ( ( 𝑧 − - 𝐵 ) ∈ 𝑦 ∧ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) }
26 23 25 eqtr4i ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∩ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } } ) = { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) }
27 22 26 eqtrdi ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∩ 𝐴 ) = { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) } )
28 17 9 27 ovolshft ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) = ( vol* ‘ ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∩ 𝐴 ) ) )
29 7 ssdifssd ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ⊆ ℝ )
30 21 difeq2d ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∖ 𝐴 ) = ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∖ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } } ) )
31 difrab ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∖ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } } ) = { 𝑧 ∈ ℝ ∣ ( ( 𝑧 − - 𝐵 ) ∈ 𝑦 ∧ ¬ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) }
32 eldif ( ( 𝑧 − - 𝐵 ) ∈ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ↔ ( ( 𝑧 − - 𝐵 ) ∈ 𝑦 ∧ ¬ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) )
33 32 rabbii { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) } = { 𝑧 ∈ ℝ ∣ ( ( 𝑧 − - 𝐵 ) ∈ 𝑦 ∧ ¬ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) }
34 31 33 eqtr4i ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∖ { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } } ) = { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) }
35 30 34 eqtrdi ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∖ 𝐴 ) = { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) } )
36 29 9 35 ovolshft ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) = ( vol* ‘ ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∖ 𝐴 ) ) )
37 28 36 oveq12d ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) + ( vol* ‘ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) ) = ( ( vol* ‘ ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∩ 𝐴 ) ) + ( vol* ‘ ( { 𝑧 ∈ ℝ ∣ ( 𝑧 − - 𝐵 ) ∈ 𝑦 } ∖ 𝐴 ) ) ) )
38 15 11 37 3eqtr4d ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ⊆ ℝ ∧ ( vol* ‘ 𝑦 ) ∈ ℝ ) ) → ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) + ( vol* ‘ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) ) )
39 38 expr ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ⊆ ℝ ) → ( ( vol* ‘ 𝑦 ) ∈ ℝ → ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) + ( vol* ‘ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) ) ) )
40 3 39 sylan2 ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ 𝒫 ℝ ) → ( ( vol* ‘ 𝑦 ) ∈ ℝ → ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) + ( vol* ‘ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) ) ) )
41 40 ralrimiva ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) → ∀ 𝑦 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑦 ) ∈ ℝ → ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) + ( vol* ‘ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) ) ) )
42 ismbl ( { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ∈ dom vol ↔ ( { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ⊆ ℝ ∧ ∀ 𝑦 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑦 ) ∈ ℝ → ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) + ( vol* ‘ ( 𝑦 ∖ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ) ) ) ) ) )
43 2 41 42 sylanbrc ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) → { 𝑥 ∈ ℝ ∣ ( 𝑥𝐵 ) ∈ 𝐴 } ∈ dom vol )