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