Proof of Theorem itg2const
Step | Hyp | Ref
| Expression |
1 | | reex 9906 |
. . . . . . 7
⊢ ℝ
∈ V |
2 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → ℝ ∈ V) |
3 | | simpl3 1059 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) ∧ 𝑥
∈ ℝ) → 𝐵
∈ (0[,)+∞)) |
4 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
5 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
6 | 4, 5 | keepel 4105 |
. . . . . . 7
⊢ if(𝑥 ∈ 𝐴, 1, 0) ∈ ℝ |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) ∧ 𝑥
∈ ℝ) → if(𝑥
∈ 𝐴, 1, 0) ∈
ℝ) |
8 | | fconstmpt 5085 |
. . . . . . 7
⊢ (ℝ
× {𝐵}) = (𝑥 ∈ ℝ ↦ 𝐵) |
9 | 8 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (ℝ × {𝐵}) = (𝑥 ∈ ℝ ↦ 𝐵)) |
10 | | eqidd 2611 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 1, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0))) |
11 | 2, 3, 7, 9, 10 | offval2 6812 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → ((ℝ × {𝐵}) ∘𝑓 ·
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 1, 0))) = (𝑥 ∈ ℝ ↦ (𝐵 · if(𝑥 ∈ 𝐴, 1, 0)))) |
12 | | ovif2 6636 |
. . . . . . 7
⊢ (𝐵 · if(𝑥 ∈ 𝐴, 1, 0)) = if(𝑥 ∈ 𝐴, (𝐵 · 1), (𝐵 · 0)) |
13 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → 𝐵
∈ (0[,)+∞)) |
14 | | elrege0 12149 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (0[,)+∞) ↔
(𝐵 ∈ ℝ ∧ 0
≤ 𝐵)) |
15 | 13, 14 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝐵
∈ ℝ ∧ 0 ≤ 𝐵)) |
16 | 15 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → 𝐵
∈ ℝ) |
17 | 16 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → 𝐵
∈ ℂ) |
18 | 17 | mulid1d 9936 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝐵
· 1) = 𝐵) |
19 | 17 | mul01d 10114 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝐵
· 0) = 0) |
20 | 18, 19 | ifeq12d 4056 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → if(𝑥
∈ 𝐴, (𝐵 · 1), (𝐵 · 0)) = if(𝑥 ∈ 𝐴, 𝐵, 0)) |
21 | 12, 20 | syl5eq 2656 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝐵
· if(𝑥 ∈ 𝐴, 1, 0)) = if(𝑥 ∈ 𝐴, 𝐵, 0)) |
22 | 21 | mpteq2dv 4673 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝑥
∈ ℝ ↦ (𝐵
· if(𝑥 ∈ 𝐴, 1, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
23 | 11, 22 | eqtrd 2644 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → ((ℝ × {𝐵}) ∘𝑓 ·
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 1, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
24 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)) |
25 | 24 | i1f1 23263 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → (𝑥 ∈
ℝ ↦ if(𝑥 ∈
𝐴, 1, 0)) ∈ dom
∫1) |
26 | 25 | 3adant3 1074 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 1, 0)) ∈ dom
∫1) |
27 | 26, 16 | i1fmulc 23276 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → ((ℝ × {𝐵}) ∘𝑓 ·
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 1, 0))) ∈ dom
∫1) |
28 | 23, 27 | eqeltrrd 2689 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)) ∈ dom
∫1) |
29 | 15 | simprd 478 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → 0 ≤ 𝐵) |
30 | | 0le0 10987 |
. . . . . 6
⊢ 0 ≤
0 |
31 | | breq2 4587 |
. . . . . . 7
⊢ (𝐵 = if(𝑥 ∈ 𝐴, 𝐵, 0) → (0 ≤ 𝐵 ↔ 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
32 | | breq2 4587 |
. . . . . . 7
⊢ (0 =
if(𝑥 ∈ 𝐴, 𝐵, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
33 | 31, 32 | ifboth 4074 |
. . . . . 6
⊢ ((0 ≤
𝐵 ∧ 0 ≤ 0) → 0
≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
34 | 29, 30, 33 | sylancl 693 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
35 | 34 | ralrimivw 2950 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
36 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
37 | 36 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → ℝ ⊆ ℂ) |
38 | 16 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) ∧ 𝑥
∈ ℝ) → 𝐵
∈ ℝ) |
39 | | ifcl 4080 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(𝑥 ∈
𝐴, 𝐵, 0) ∈ ℝ) |
40 | 38, 5, 39 | sylancl 693 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) ∧ 𝑥
∈ ℝ) → if(𝑥
∈ 𝐴, 𝐵, 0) ∈ ℝ) |
41 | 40 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ ℝ) |
42 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) |
43 | 42 | fnmpt 5933 |
. . . . . . 7
⊢
(∀𝑥 ∈
ℝ if(𝑥 ∈ 𝐴, 𝐵, 0) ∈ ℝ → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) Fn ℝ) |
44 | 41, 43 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)) Fn ℝ) |
45 | 37, 44 | 0pledm 23246 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (0𝑝 ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0)) ↔ (ℝ × {0})
∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) |
46 | 5 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) ∧ 𝑥
∈ ℝ) → 0 ∈ ℝ) |
47 | | fconstmpt 5085 |
. . . . . . 7
⊢ (ℝ
× {0}) = (𝑥 ∈
ℝ ↦ 0) |
48 | 47 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (ℝ × {0}) = (𝑥 ∈ ℝ ↦ 0)) |
49 | | eqidd 2611 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
50 | 2, 46, 40, 48, 49 | ofrfval2 6813 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → ((ℝ × {0}) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
51 | 45, 50 | bitrd 267 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (0𝑝 ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ 𝐴, 𝐵, 0))) |
52 | 35, 51 | mpbird 246 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → 0𝑝 ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, 𝐵, 0))) |
53 | | itg2itg1 23309 |
. . 3
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) |
54 | 28, 52, 53 | syl2anc 691 |
. 2
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0)))) |
55 | 26, 16 | itg1mulc 23277 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫1‘((ℝ × {𝐵}) ∘𝑓
· (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, 1, 0)))) = (𝐵 · (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0))))) |
56 | 23 | fveq2d 6107 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫1‘((ℝ × {𝐵}) ∘𝑓
· (𝑥 ∈ ℝ
↦ if(𝑥 ∈ 𝐴, 1, 0)))) =
(∫1‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, 𝐵, 0)))) |
57 | 24 | itg11 23264 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0))) = (vol‘𝐴)) |
58 | 57 | 3adant3 1074 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0))) = (vol‘𝐴)) |
59 | 58 | oveq2d 6565 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (𝐵
· (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)))) = (𝐵 · (vol‘𝐴))) |
60 | 55, 56, 59 | 3eqtr3d 2652 |
. 2
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫1‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) = (𝐵 · (vol‘𝐴))) |
61 | 54, 60 | eqtrd 2644 |
1
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ ∧ 𝐵 ∈
(0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) = (𝐵 · (vol‘𝐴))) |