Step | Hyp | Ref
| Expression |
1 | | ovol0 23261 |
. . . . 5
⊢
(vol*‘∅) = 0 |
2 | | 0mbl 23307 |
. . . . . 6
⊢ ∅
∈ dom vol |
3 | | mblvol 23298 |
. . . . . 6
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢
(vol‘∅) = (vol*‘∅) |
5 | | itg10 23455 |
. . . . 5
⊢
(∫1‘(ℝ × {0})) = 0 |
6 | 1, 4, 5 | 3eqtr4ri 2655 |
. . . 4
⊢
(∫1‘(ℝ × {0})) =
(vol‘∅) |
7 | | noel 3919 |
. . . . . . . . 9
⊢ ¬
𝑥 ∈
∅ |
8 | | eleq2 2690 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ∅)) |
9 | 7, 8 | mtbiri 317 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴) |
10 | 9 | iffalsed 4097 |
. . . . . . 7
⊢ (𝐴 = ∅ → if(𝑥 ∈ 𝐴, 1, 0) = 0) |
11 | 10 | mpteq2dv 4745 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)) = (𝑥 ∈ ℝ ↦ 0)) |
12 | | i1f1.1 |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0)) |
13 | | fconstmpt 5163 |
. . . . . 6
⊢ (ℝ
× {0}) = (𝑥 ∈
ℝ ↦ 0) |
14 | 11, 12, 13 | 3eqtr4g 2681 |
. . . . 5
⊢ (𝐴 = ∅ → 𝐹 = (ℝ ×
{0})) |
15 | 14 | fveq2d 6195 |
. . . 4
⊢ (𝐴 = ∅ →
(∫1‘𝐹)
= (∫1‘(ℝ × {0}))) |
16 | | fveq2 6191 |
. . . 4
⊢ (𝐴 = ∅ →
(vol‘𝐴) =
(vol‘∅)) |
17 | 6, 15, 16 | 3eqtr4a 2682 |
. . 3
⊢ (𝐴 = ∅ →
(∫1‘𝐹)
= (vol‘𝐴)) |
18 | 17 | a1i 11 |
. 2
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → (𝐴 =
∅ → (∫1‘𝐹) = (vol‘𝐴))) |
19 | | n0 3931 |
. . 3
⊢ (𝐴 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐴) |
20 | 12 | i1f1 23457 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → 𝐹 ∈
dom ∫1) |
21 | 20 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → 𝐹 ∈ dom
∫1) |
22 | | itg1val 23450 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) = Σ𝑧 ∈ (ran 𝐹 ∖ {0})(𝑧 · (vol‘(◡𝐹 “ {𝑧})))) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) →
(∫1‘𝐹)
= Σ𝑧 ∈ (ran
𝐹 ∖ {0})(𝑧 · (vol‘(◡𝐹 “ {𝑧})))) |
24 | 12 | i1f1lem 23456 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℝ⟶{0, 1} ∧
(𝐴 ∈ dom vol →
(◡𝐹 “ {1}) = 𝐴)) |
25 | 24 | simpli 474 |
. . . . . . . . . . . . 13
⊢ 𝐹:ℝ⟶{0,
1} |
26 | | frn 6053 |
. . . . . . . . . . . . 13
⊢ (𝐹:ℝ⟶{0, 1} →
ran 𝐹 ⊆ {0,
1}) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ran 𝐹 ⊆ {0, 1} |
28 | | ssdif 3745 |
. . . . . . . . . . . 12
⊢ (ran
𝐹 ⊆ {0, 1} →
(ran 𝐹 ∖ {0}) ⊆
({0, 1} ∖ {0})) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ran
𝐹 ∖ {0}) ⊆ ({0,
1} ∖ {0}) |
30 | | difprsnss 4329 |
. . . . . . . . . . 11
⊢ ({0, 1}
∖ {0}) ⊆ {1} |
31 | 29, 30 | sstri 3612 |
. . . . . . . . . 10
⊢ (ran
𝐹 ∖ {0}) ⊆
{1} |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (ran 𝐹 ∖ {0}) ⊆
{1}) |
33 | | mblss 23299 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → 𝐴 ⊆
ℝ) |
35 | 34 | sselda 3603 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → 𝑦 ∈
ℝ) |
36 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
37 | 36 | ifbid 4108 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ 𝐴, 1, 0) = if(𝑦 ∈ 𝐴, 1, 0)) |
38 | | 1ex 10035 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
V |
39 | | c0ex 10034 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
V |
40 | 38, 39 | ifex 4156 |
. . . . . . . . . . . . . . 15
⊢ if(𝑦 ∈ 𝐴, 1, 0) ∈ V |
41 | 37, 12, 40 | fvmpt 6282 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → (𝐹‘𝑦) = if(𝑦 ∈ 𝐴, 1, 0)) |
42 | 35, 41 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (𝐹‘𝑦) = if(𝑦 ∈ 𝐴, 1, 0)) |
43 | | iftrue 4092 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐴 → if(𝑦 ∈ 𝐴, 1, 0) = 1) |
44 | 43 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → if(𝑦 ∈ 𝐴, 1, 0) = 1) |
45 | 42, 44 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (𝐹‘𝑦) = 1) |
46 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℝ⟶{0, 1} →
𝐹 Fn
ℝ) |
47 | 25, 46 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ 𝐹 Fn ℝ |
48 | | fnfvelrn 6356 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn ℝ ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ran 𝐹) |
49 | 47, 35, 48 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (𝐹‘𝑦) ∈ ran 𝐹) |
50 | 45, 49 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → 1 ∈ ran
𝐹) |
51 | | ax-1ne0 10005 |
. . . . . . . . . . . 12
⊢ 1 ≠
0 |
52 | 51 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → 1 ≠
0) |
53 | | eldifsn 4317 |
. . . . . . . . . . 11
⊢ (1 ∈
(ran 𝐹 ∖ {0}) ↔
(1 ∈ ran 𝐹 ∧ 1
≠ 0)) |
54 | 50, 52, 53 | sylanbrc 698 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → 1 ∈ (ran
𝐹 ∖
{0})) |
55 | 54 | snssd 4340 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → {1} ⊆ (ran
𝐹 ∖
{0})) |
56 | 32, 55 | eqssd 3620 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (ran 𝐹 ∖ {0}) =
{1}) |
57 | 56 | sumeq1d 14431 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → Σ𝑧 ∈ (ran 𝐹 ∖ {0})(𝑧 · (vol‘(◡𝐹 “ {𝑧}))) = Σ𝑧 ∈ {1} (𝑧 · (vol‘(◡𝐹 “ {𝑧})))) |
58 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
59 | 24 | simpri 478 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom vol → (◡𝐹 “ {1}) = 𝐴) |
60 | 59 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (◡𝐹 “ {1}) = 𝐴) |
61 | 60 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (vol‘(◡𝐹 “ {1})) = (vol‘𝐴)) |
62 | 61 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (1 ·
(vol‘(◡𝐹 “ {1}))) = (1 ·
(vol‘𝐴))) |
63 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (vol‘𝐴) ∈
ℝ) |
64 | 63 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (vol‘𝐴) ∈
ℂ) |
65 | 64 | mulid2d 10058 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (1 ·
(vol‘𝐴)) =
(vol‘𝐴)) |
66 | 62, 65 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (1 ·
(vol‘(◡𝐹 “ {1}))) = (vol‘𝐴)) |
67 | 66, 64 | eqeltrd 2701 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → (1 ·
(vol‘(◡𝐹 “ {1}))) ∈
ℂ) |
68 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑧 = 1 → 𝑧 = 1) |
69 | | sneq 4187 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 1 → {𝑧} = {1}) |
70 | 69 | imaeq2d 5466 |
. . . . . . . . . . . 12
⊢ (𝑧 = 1 → (◡𝐹 “ {𝑧}) = (◡𝐹 “ {1})) |
71 | 70 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑧 = 1 → (vol‘(◡𝐹 “ {𝑧})) = (vol‘(◡𝐹 “ {1}))) |
72 | 68, 71 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑧 = 1 → (𝑧 · (vol‘(◡𝐹 “ {𝑧}))) = (1 · (vol‘(◡𝐹 “ {1})))) |
73 | 72 | sumsn 14475 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (1 · (vol‘(◡𝐹 “ {1}))) ∈ ℂ) →
Σ𝑧 ∈ {1} (𝑧 · (vol‘(◡𝐹 “ {𝑧}))) = (1 · (vol‘(◡𝐹 “ {1})))) |
74 | 58, 67, 73 | sylancr 695 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → Σ𝑧 ∈ {1} (𝑧 · (vol‘(◡𝐹 “ {𝑧}))) = (1 · (vol‘(◡𝐹 “ {1})))) |
75 | 74, 66 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → Σ𝑧 ∈ {1} (𝑧 · (vol‘(◡𝐹 “ {𝑧}))) = (vol‘𝐴)) |
76 | 57, 75 | eqtrd 2656 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) → Σ𝑧 ∈ (ran 𝐹 ∖ {0})(𝑧 · (vol‘(◡𝐹 “ {𝑧}))) = (vol‘𝐴)) |
77 | 23, 76 | eqtrd 2656 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) ∧ 𝑦 ∈
𝐴) →
(∫1‘𝐹)
= (vol‘𝐴)) |
78 | 77 | ex 450 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → (𝑦 ∈
𝐴 →
(∫1‘𝐹)
= (vol‘𝐴))) |
79 | 78 | exlimdv 1861 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → (∃𝑦
𝑦 ∈ 𝐴 → (∫1‘𝐹) = (vol‘𝐴))) |
80 | 19, 79 | syl5bi 232 |
. 2
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → (𝐴 ≠
∅ → (∫1‘𝐹) = (vol‘𝐴))) |
81 | 18, 80 | pm2.61dne 2880 |
1
⊢ ((𝐴 ∈ dom vol ∧
(vol‘𝐴) ∈
ℝ) → (∫1‘𝐹) = (vol‘𝐴)) |