Proof of Theorem ismbl2
Step | Hyp | Ref
| Expression |
1 | | ismbl 23101 |
. 2
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))))) |
2 | | elpwi 4117 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 ℝ →
𝑥 ⊆
ℝ) |
3 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘𝑥) ∈ ℝ) |
4 | | inss1 3795 |
. . . . . . . . . . . 12
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
5 | | ovolsscl 23061 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∩ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∩ 𝐴)) ∈
ℝ) |
6 | 4, 5 | mp3an1 1403 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
7 | 6 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
8 | | difss 3699 |
. . . . . . . . . . . 12
⊢ (𝑥 ∖ 𝐴) ⊆ 𝑥 |
9 | | ovolsscl 23061 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∖ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∖
𝐴)) ∈
ℝ) |
10 | 8, 9 | mp3an1 1403 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) |
11 | 10 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) |
12 | 7, 11 | readdcld 9948 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ∈ ℝ) |
13 | 3, 12 | letri3d 10058 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ↔ ((vol*‘𝑥) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ∧ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
14 | | inundif 3998 |
. . . . . . . . . . 11
⊢ ((𝑥 ∩ 𝐴) ∪ (𝑥 ∖ 𝐴)) = 𝑥 |
15 | 14 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(vol*‘((𝑥
∩ 𝐴) ∪ (𝑥 ∖ 𝐴))) = (vol*‘𝑥) |
16 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → 𝑥 ⊆
ℝ) |
17 | 4, 16 | syl5ss 3579 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (𝑥 ∩
𝐴) ⊆
ℝ) |
18 | 8, 16 | syl5ss 3579 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (𝑥 ∖
𝐴) ⊆
ℝ) |
19 | | ovolun 23074 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) ∧ ((𝑥 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ)) →
(vol*‘((𝑥 ∩ 𝐴) ∪ (𝑥 ∖ 𝐴))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
20 | 17, 7, 18, 11, 19 | syl22anc 1319 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘((𝑥 ∩ 𝐴) ∪ (𝑥 ∖ 𝐴))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
21 | 15, 20 | syl5eqbrr 4619 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘𝑥) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
22 | 21 | biantrurd 528 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥) ↔ ((vol*‘𝑥) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ∧ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
23 | 13, 22 | bitr4d 270 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ↔ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) |
24 | 23 | expr 641 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ) →
((vol*‘𝑥) ∈
ℝ → ((vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ↔ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
25 | 24 | pm5.74d 261 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ) →
(((vol*‘𝑥) ∈
ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) ↔ ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
26 | 2, 25 | sylan2 490 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝒫 ℝ)
→ (((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) ↔ ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
27 | 26 | ralbidva 2968 |
. . 3
⊢ (𝐴 ⊆ ℝ →
(∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) ↔ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ →
((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
28 | 27 | pm5.32i 667 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))))) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |
29 | 1, 28 | bitri 263 |
1
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) |