| Step | Hyp | Ref
| Expression |
| 1 | | i1frn 25712 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
| 2 | | difss 4136 |
. . . . 5
⊢ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹 |
| 3 | | ssfi 9213 |
. . . . 5
⊢ ((ran
𝐹 ∈ Fin ∧ (ran
𝐹 ∖ {0}) ⊆ ran
𝐹) → (ran 𝐹 ∖ {0}) ∈
Fin) |
| 4 | 1, 2, 3 | sylancl 586 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (ran 𝐹 ∖ {0})
∈ Fin) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → (ran 𝐹 ∖ {0}) ∈ Fin) |
| 6 | | i1ff 25711 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
| 7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → 𝐹:ℝ⟶ℝ) |
| 8 | 7 | frnd 6744 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → ran 𝐹 ⊆ ℝ) |
| 9 | 8 | ssdifssd 4147 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → (ran 𝐹 ∖ {0}) ⊆
ℝ) |
| 10 | 9 | sselda 3983 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → 𝑥 ∈ ℝ) |
| 11 | | i1fima2sn 25715 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
| 12 | 11 | adantlr 715 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
| 13 | 10, 12 | remulcld 11291 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (𝑥 · (vol‘(◡𝐹 “ {𝑥}))) ∈ ℝ) |
| 14 | | eldifi 4131 |
. . . . 5
⊢ (𝑥 ∈ (ran 𝐹 ∖ {0}) → 𝑥 ∈ ran 𝐹) |
| 15 | | 0cn 11253 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
| 16 | | fnconstg 6796 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℂ → (ℂ × {0}) Fn ℂ) |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℂ
× {0}) Fn ℂ |
| 18 | | df-0p 25705 |
. . . . . . . . . . . 12
⊢
0𝑝 = (ℂ × {0}) |
| 19 | 18 | fneq1i 6665 |
. . . . . . . . . . 11
⊢
(0𝑝 Fn ℂ ↔ (ℂ × {0}) Fn
ℂ) |
| 20 | 17, 19 | mpbir 231 |
. . . . . . . . . 10
⊢
0𝑝 Fn ℂ |
| 21 | 20 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 Fn ℂ) |
| 22 | 6 | ffnd 6737 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 Fn
ℝ) |
| 23 | | cnex 11236 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
| 24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ℂ ∈ V) |
| 25 | | reex 11246 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
| 26 | 25 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ℝ ∈ V) |
| 27 | | ax-resscn 11212 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
| 28 | | sseqin2 4223 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ) |
| 29 | 27, 28 | mpbi 230 |
. . . . . . . . 9
⊢ (ℂ
∩ ℝ) = ℝ |
| 30 | | 0pval 25706 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ →
(0𝑝‘𝑦) = 0) |
| 31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑦 ∈ ℂ)
→ (0𝑝‘𝑦) = 0) |
| 32 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑦 ∈ ℝ)
→ (𝐹‘𝑦) = (𝐹‘𝑦)) |
| 33 | 21, 22, 24, 26, 29, 31, 32 | ofrfval 7707 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘r ≤ 𝐹 ↔ ∀𝑦 ∈ ℝ 0 ≤ (𝐹‘𝑦))) |
| 34 | 33 | biimpa 476 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → ∀𝑦 ∈ ℝ 0 ≤ (𝐹‘𝑦)) |
| 35 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → 𝐹 Fn ℝ) |
| 36 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑦) → (0 ≤ 𝑥 ↔ 0 ≤ (𝐹‘𝑦))) |
| 37 | 36 | ralrn 7108 |
. . . . . . . 8
⊢ (𝐹 Fn ℝ →
(∀𝑥 ∈ ran 𝐹0 ≤ 𝑥 ↔ ∀𝑦 ∈ ℝ 0 ≤ (𝐹‘𝑦))) |
| 38 | 35, 37 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → (∀𝑥 ∈ ran 𝐹0 ≤ 𝑥 ↔ ∀𝑦 ∈ ℝ 0 ≤ (𝐹‘𝑦))) |
| 39 | 34, 38 | mpbird 257 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → ∀𝑥 ∈ ran 𝐹0 ≤ 𝑥) |
| 40 | 39 | r19.21bi 3251 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) ∧ 𝑥 ∈ ran 𝐹) → 0 ≤ 𝑥) |
| 41 | 14, 40 | sylan2 593 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → 0 ≤ 𝑥) |
| 42 | | i1fima 25713 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {𝑥}) ∈ dom vol) |
| 43 | 42 | ad2antrr 726 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol) |
| 44 | | mblss 25566 |
. . . . . . 7
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ) |
| 45 | | ovolge0 25516 |
. . . . . . 7
⊢ ((◡𝐹 “ {𝑥}) ⊆ ℝ → 0 ≤
(vol*‘(◡𝐹 “ {𝑥}))) |
| 46 | 44, 45 | syl 17 |
. . . . . 6
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → 0 ≤
(vol*‘(◡𝐹 “ {𝑥}))) |
| 47 | | mblvol 25565 |
. . . . . 6
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ {𝑥}))) |
| 48 | 46, 47 | breqtrrd 5171 |
. . . . 5
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → 0 ≤
(vol‘(◡𝐹 “ {𝑥}))) |
| 49 | 43, 48 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → 0 ≤
(vol‘(◡𝐹 “ {𝑥}))) |
| 50 | 10, 12, 41, 49 | mulge0d 11840 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → 0 ≤ (𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
| 51 | 5, 13, 50 | fsumge0 15831 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → 0 ≤ Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
| 52 | | itg1val 25718 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) = Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
| 53 | 52 | adantr 480 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → (∫1‘𝐹) = Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥})))) |
| 54 | 51, 53 | breqtrrd 5171 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ 0𝑝 ∘r ≤ 𝐹) → 0 ≤
(∫1‘𝐹)) |