Proof of Theorem ismbl4
Step | Hyp | Ref
| Expression |
1 | | ismbl3 43527 |
. 2
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘(𝑥
∩ 𝐴))
+𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))) |
2 | | elpwi 4542 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 ℝ →
𝑥 ⊆
ℝ) |
3 | | ovolcl 24642 |
. . . . . . . . 9
⊢ (𝑥 ⊆ ℝ →
(vol*‘𝑥) ∈
ℝ*) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 ℝ →
(vol*‘𝑥) ∈
ℝ*) |
5 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥)) → (vol*‘𝑥) ∈
ℝ*) |
6 | | inss1 4162 |
. . . . . . . . . . 11
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
7 | 6, 2 | sstrid 3932 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 ℝ →
(𝑥 ∩ 𝐴) ⊆ ℝ) |
8 | | ovolcl 24642 |
. . . . . . . . . 10
⊢ ((𝑥 ∩ 𝐴) ⊆ ℝ → (vol*‘(𝑥 ∩ 𝐴)) ∈
ℝ*) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 ℝ →
(vol*‘(𝑥 ∩ 𝐴)) ∈
ℝ*) |
10 | 2 | ssdifssd 4077 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 ℝ →
(𝑥 ∖ 𝐴) ⊆
ℝ) |
11 | | ovolcl 24642 |
. . . . . . . . . 10
⊢ ((𝑥 ∖ 𝐴) ⊆ ℝ → (vol*‘(𝑥 ∖ 𝐴)) ∈
ℝ*) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 ℝ →
(vol*‘(𝑥 ∖
𝐴)) ∈
ℝ*) |
13 | 9, 12 | xaddcld 13035 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 ℝ →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ∈
ℝ*) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥)) → ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ∈
ℝ*) |
15 | 2 | ovolsplit 43529 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 ℝ →
(vol*‘𝑥) ≤
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴)))) |
16 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥)) → (vol*‘𝑥) ≤ ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴)))) |
17 | | simpr 485 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥)) → ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) |
18 | 5, 14, 16, 17 | xrletrid 12889 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥)) → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴)))) |
19 | 18 | ex 413 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 ℝ →
(((vol*‘(𝑥 ∩
𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥) → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))))) |
20 | 13 | xrleidd 12886 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 ℝ →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴)))) |
21 | 20 | adantr 481 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) =
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴)))) →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴)))) |
22 | | id 22 |
. . . . . . . . 9
⊢
((vol*‘𝑥) =
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) →
(vol*‘𝑥) =
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴)))) |
23 | 22 | eqcomd 2744 |
. . . . . . . 8
⊢
((vol*‘𝑥) =
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) = (vol*‘𝑥)) |
24 | 23 | adantl 482 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) =
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴)))) →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) = (vol*‘𝑥)) |
25 | 21, 24 | breqtrd 5100 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℝ ∧
(vol*‘𝑥) =
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴)))) →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥)) |
26 | 25 | ex 413 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 ℝ →
((vol*‘𝑥) =
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) →
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥))) |
27 | 19, 26 | impbid 211 |
. . . 4
⊢ (𝑥 ∈ 𝒫 ℝ →
(((vol*‘(𝑥 ∩
𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))) ≤ (vol*‘𝑥) ↔ (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))))) |
28 | 27 | ralbiia 3091 |
. . 3
⊢
(∀𝑥 ∈
𝒫 ℝ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥) ↔ ∀𝑥 ∈ 𝒫 ℝ(vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) +𝑒 (vol*‘(𝑥 ∖ 𝐴)))) |
29 | 28 | anbi2i 623 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ((vol*‘(𝑥
∩ 𝐴))
+𝑒 (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫
ℝ(vol*‘𝑥) =
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))))) |
30 | 1, 29 | bitri 274 |
1
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧
∀𝑥 ∈ 𝒫
ℝ(vol*‘𝑥) =
((vol*‘(𝑥 ∩ 𝐴)) +𝑒
(vol*‘(𝑥 ∖
𝐴))))) |