Proof of Theorem itg1val2
Step | Hyp | Ref
| Expression |
1 | | itg1val 23256 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) = Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
2 | 1 | adantr 480 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) →
(∫1‘𝐹)
= Σ𝑥 ∈ (ran
𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
3 | | simpr2 1061 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) → (ran
𝐹 ∖ {0}) ⊆
𝐴) |
4 | 3 | sselda 3568 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → 𝑥 ∈ 𝐴) |
5 | | simpr3 1062 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) →
𝐴 ⊆ (ℝ ∖
{0})) |
6 | 5 | sselda 3568 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (ℝ ∖
{0})) |
7 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑥 ∈ (ℝ ∖ {0})
→ 𝑥 ∈
ℝ) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
9 | | i1fima2sn 23253 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ (ℝ
∖ {0})) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
10 | 9 | adantlr 747 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (ℝ ∖ {0}))
→ (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
11 | 6, 10 | syldan 486 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
12 | 8, 11 | remulcld 9949 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → (𝑥 · (vol‘(◡𝐹 “ {𝑥}))) ∈ ℝ) |
13 | 12 | recnd 9947 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → (𝑥 · (vol‘(◡𝐹 “ {𝑥}))) ∈ ℂ) |
14 | 4, 13 | syldan 486 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (𝑥 · (vol‘(◡𝐹 “ {𝑥}))) ∈ ℂ) |
15 | | i1ff 23249 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
16 | 15 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → 𝐹:ℝ⟶ℝ) |
17 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
18 | | dffn3 5967 |
. . . . . . . . . 10
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
19 | 17, 18 | sylib 207 |
. . . . . . . . 9
⊢ (𝐹:ℝ⟶ℝ →
𝐹:ℝ⟶ran 𝐹) |
20 | 16, 19 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → 𝐹:ℝ⟶ran 𝐹) |
21 | | eldifn 3695 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0})) → ¬ 𝑥 ∈ (ran 𝐹 ∖ {0})) |
22 | 21 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → ¬ 𝑥 ∈ (ran 𝐹 ∖ {0})) |
23 | | simplr3 1098 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → 𝐴 ⊆ (ℝ ∖
{0})) |
24 | 23 | ssdifssd 3710 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (𝐴 ∖ (ran 𝐹 ∖ {0})) ⊆ (ℝ ∖
{0})) |
25 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) |
26 | 24, 25 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → 𝑥 ∈ (ℝ ∖
{0})) |
27 | | eldifn 3695 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (ℝ ∖ {0})
→ ¬ 𝑥 ∈
{0}) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → ¬ 𝑥 ∈ {0}) |
29 | 28 | biantrud 527 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (𝑥 ∈ ran 𝐹 ↔ (𝑥 ∈ ran 𝐹 ∧ ¬ 𝑥 ∈ {0}))) |
30 | | eldif 3550 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ran 𝐹 ∖ {0}) ↔ (𝑥 ∈ ran 𝐹 ∧ ¬ 𝑥 ∈ {0})) |
31 | 29, 30 | syl6rbbr 278 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (𝑥 ∈ (ran 𝐹 ∖ {0}) ↔ 𝑥 ∈ ran 𝐹)) |
32 | 22, 31 | mtbid 313 |
. . . . . . . . 9
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → ¬ 𝑥 ∈ ran 𝐹) |
33 | | disjsn 4192 |
. . . . . . . . 9
⊢ ((ran
𝐹 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ran 𝐹) |
34 | 32, 33 | sylibr 223 |
. . . . . . . 8
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (ran 𝐹 ∩ {𝑥}) = ∅) |
35 | | fimacnvdisj 5996 |
. . . . . . . 8
⊢ ((𝐹:ℝ⟶ran 𝐹 ∧ (ran 𝐹 ∩ {𝑥}) = ∅) → (◡𝐹 “ {𝑥}) = ∅) |
36 | 20, 34, 35 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (◡𝐹 “ {𝑥}) = ∅) |
37 | 36 | fveq2d 6107 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (vol‘(◡𝐹 “ {𝑥})) = (vol‘∅)) |
38 | | 0mbl 23114 |
. . . . . . . 8
⊢ ∅
∈ dom vol |
39 | | mblvol 23105 |
. . . . . . . 8
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . 7
⊢
(vol‘∅) = (vol*‘∅) |
41 | | ovol0 23068 |
. . . . . . 7
⊢
(vol*‘∅) = 0 |
42 | 40, 41 | eqtri 2632 |
. . . . . 6
⊢
(vol‘∅) = 0 |
43 | 37, 42 | syl6eq 2660 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (vol‘(◡𝐹 “ {𝑥})) = 0) |
44 | 43 | oveq2d 6565 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (𝑥 · (vol‘(◡𝐹 “ {𝑥}))) = (𝑥 · 0)) |
45 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0})) → 𝑥 ∈ 𝐴) |
46 | 45, 8 | sylan2 490 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → 𝑥 ∈ ℝ) |
47 | 46 | recnd 9947 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → 𝑥 ∈ ℂ) |
48 | 47 | mul01d 10114 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (𝑥 · 0) = 0) |
49 | 44, 48 | eqtrd 2644 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) ∧ 𝑥 ∈ (𝐴 ∖ (ran 𝐹 ∖ {0}))) → (𝑥 · (vol‘(◡𝐹 “ {𝑥}))) = 0) |
50 | | simpr1 1060 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) →
𝐴 ∈
Fin) |
51 | 3, 14, 49, 50 | fsumss 14303 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) →
Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥}))) = Σ𝑥 ∈ 𝐴 (𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
52 | 2, 51 | eqtrd 2644 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ (𝐴 ∈ Fin ∧
(ran 𝐹 ∖ {0}) ⊆
𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) →
(∫1‘𝐹)
= Σ𝑥 ∈ 𝐴 (𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |