Step | Hyp | Ref
| Expression |
1 | | difssd 3700 |
. 2
⊢ (𝐴 ∈ dom vol → (ℝ
∖ 𝐴) ⊆
ℝ) |
2 | | elpwi 4117 |
. . . 4
⊢ (𝑥 ∈ 𝒫 ℝ →
𝑥 ⊆
ℝ) |
3 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
4 | | ovolsscl 23061 |
. . . . . . . . . 10
⊢ (((𝑥 ∩ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∩ 𝐴)) ∈
ℝ) |
5 | 3, 4 | mp3an1 1403 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
6 | 5 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
7 | 6 | recnd 9947 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℂ) |
8 | | difss 3699 |
. . . . . . . . . 10
⊢ (𝑥 ∖ 𝐴) ⊆ 𝑥 |
9 | | ovolsscl 23061 |
. . . . . . . . . 10
⊢ (((𝑥 ∖ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∖
𝐴)) ∈
ℝ) |
10 | 8, 9 | mp3an1 1403 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) |
11 | 10 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) |
12 | 11 | recnd 9947 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℂ) |
13 | 7, 12 | addcomd 10117 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) = ((vol*‘(𝑥 ∖ 𝐴)) + (vol*‘(𝑥 ∩ 𝐴)))) |
14 | | mblsplit 23107 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
15 | | indifcom 3831 |
. . . . . . . . 9
⊢ (ℝ
∩ (𝑥 ∖ 𝐴)) = (𝑥 ∩ (ℝ ∖ 𝐴)) |
16 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → 𝑥 ⊆
ℝ) |
17 | 16 | ssdifssd 3710 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (𝑥 ∖
𝐴) ⊆
ℝ) |
18 | | sseqin2 3779 |
. . . . . . . . . 10
⊢ ((𝑥 ∖ 𝐴) ⊆ ℝ ↔ (ℝ ∩
(𝑥 ∖ 𝐴)) = (𝑥 ∖ 𝐴)) |
19 | 17, 18 | sylib 207 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (ℝ ∩ (𝑥 ∖ 𝐴)) = (𝑥 ∖ 𝐴)) |
20 | 15, 19 | syl5eqr 2658 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (𝑥 ∩
(ℝ ∖ 𝐴)) =
(𝑥 ∖ 𝐴)) |
21 | 20 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ (ℝ ∖ 𝐴))) = (vol*‘(𝑥 ∖ 𝐴))) |
22 | | difin 3823 |
. . . . . . . . . 10
⊢ (𝑥 ∖ (𝑥 ∩ (ℝ ∖ 𝐴))) = (𝑥 ∖ (ℝ ∖ 𝐴)) |
23 | 20 | difeq2d 3690 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (𝑥 ∖
(𝑥 ∩ (ℝ ∖
𝐴))) = (𝑥 ∖ (𝑥 ∖ 𝐴))) |
24 | 22, 23 | syl5eqr 2658 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (𝑥 ∖
(ℝ ∖ 𝐴)) =
(𝑥 ∖ (𝑥 ∖ 𝐴))) |
25 | | dfin4 3826 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝐴) = (𝑥 ∖ (𝑥 ∖ 𝐴)) |
26 | 24, 25 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (𝑥 ∖
(ℝ ∖ 𝐴)) =
(𝑥 ∩ 𝐴)) |
27 | 26 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ (ℝ ∖ 𝐴))) = (vol*‘(𝑥 ∩ 𝐴))) |
28 | 21, 27 | oveq12d 6567 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → ((vol*‘(𝑥 ∩ (ℝ ∖ 𝐴))) + (vol*‘(𝑥 ∖ (ℝ ∖ 𝐴)))) = ((vol*‘(𝑥 ∖ 𝐴)) + (vol*‘(𝑥 ∩ 𝐴)))) |
29 | 13, 14, 28 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ (ℝ ∖ 𝐴))) + (vol*‘(𝑥 ∖ (ℝ ∖ 𝐴))))) |
30 | 29 | 3expia 1259 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ) →
((vol*‘𝑥) ∈
ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ (ℝ ∖ 𝐴))) + (vol*‘(𝑥 ∖ (ℝ ∖ 𝐴)))))) |
31 | 2, 30 | sylan2 490 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝒫 ℝ)
→ ((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ (ℝ ∖ 𝐴))) + (vol*‘(𝑥 ∖ (ℝ ∖ 𝐴)))))) |
32 | 31 | ralrimiva 2949 |
. 2
⊢ (𝐴 ∈ dom vol →
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ (ℝ ∖ 𝐴))) + (vol*‘(𝑥 ∖ (ℝ ∖ 𝐴)))))) |
33 | | ismbl 23101 |
. 2
⊢ ((ℝ
∖ 𝐴) ∈ dom vol
↔ ((ℝ ∖ 𝐴)
⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ →
(vol*‘𝑥) =
((vol*‘(𝑥 ∩
(ℝ ∖ 𝐴))) +
(vol*‘(𝑥 ∖
(ℝ ∖ 𝐴))))))) |
34 | 1, 32, 33 | sylanbrc 695 |
1
⊢ (𝐴 ∈ dom vol → (ℝ
∖ 𝐴) ∈ dom
vol) |