Step |
Hyp |
Ref |
Expression |
1 |
|
reex |
⊢ ℝ ∈ V |
2 |
1
|
elpw2 |
⊢ ( 𝐵 ∈ 𝒫 ℝ ↔ 𝐵 ⊆ ℝ ) |
3 |
|
ismbl |
⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) ) |
4 |
|
fveq2 |
⊢ ( 𝑥 = 𝐵 → ( vol* ‘ 𝑥 ) = ( vol* ‘ 𝐵 ) ) |
5 |
4
|
eleq1d |
⊢ ( 𝑥 = 𝐵 → ( ( vol* ‘ 𝑥 ) ∈ ℝ ↔ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) |
6 |
|
ineq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) ) |
7 |
6
|
fveq2d |
⊢ ( 𝑥 = 𝐵 → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) = ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) ) |
8 |
|
difeq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) ) |
9 |
8
|
fveq2d |
⊢ ( 𝑥 = 𝐵 → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) = ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) |
10 |
7 9
|
oveq12d |
⊢ ( 𝑥 = 𝐵 → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) |
11 |
4 10
|
eqeq12d |
⊢ ( 𝑥 = 𝐵 → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) |
12 |
5 11
|
imbi12d |
⊢ ( 𝑥 = 𝐵 → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( ( vol* ‘ 𝐵 ) ∈ ℝ → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) ) |
13 |
12
|
rspccv |
⊢ ( ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) → ( 𝐵 ∈ 𝒫 ℝ → ( ( vol* ‘ 𝐵 ) ∈ ℝ → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) ) |
14 |
3 13
|
simplbiim |
⊢ ( 𝐴 ∈ dom vol → ( 𝐵 ∈ 𝒫 ℝ → ( ( vol* ‘ 𝐵 ) ∈ ℝ → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) ) |
15 |
2 14
|
syl5bir |
⊢ ( 𝐴 ∈ dom vol → ( 𝐵 ⊆ ℝ → ( ( vol* ‘ 𝐵 ) ∈ ℝ → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) ) |
16 |
15
|
3imp |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) |