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 )