| Step | Hyp | Ref
| Expression |
| 1 | | i1ff 25711 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
| 2 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐹:ℝ⟶ℝ) |
| 3 | 2 | ffnd 6737 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐹 Fn
ℝ) |
| 4 | | fnfvelrn 7100 |
. . . . . 6
⊢ ((𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ran 𝐹) |
| 5 | 3, 4 | sylan 580 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈ ran 𝐹) |
| 6 | | i1f0rn 25717 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0 ∈ ran 𝐹) |
| 7 | 6 | ad2antrr 726 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑥 ∈ ℝ)
→ 0 ∈ ran 𝐹) |
| 8 | 5, 7 | ifcld 4572 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑥 ∈ ℝ)
→ if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0) ∈ ran 𝐹) |
| 9 | | i1fres.1 |
. . . 4
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0)) |
| 10 | 8, 9 | fmptd 7134 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐺:ℝ⟶ran
𝐹) |
| 11 | 2 | frnd 6744 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ ran 𝐹 ⊆
ℝ) |
| 12 | 10, 11 | fssd 6753 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐺:ℝ⟶ℝ) |
| 13 | | i1frn 25712 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
| 14 | 13 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ ran 𝐹 ∈
Fin) |
| 15 | 10 | frnd 6744 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ ran 𝐺 ⊆ ran
𝐹) |
| 16 | 14, 15 | ssfid 9301 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ ran 𝐺 ∈
Fin) |
| 17 | | eleq1w 2824 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) |
| 18 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
| 19 | 17, 18 | ifbieq1d 4550 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0) = if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0)) |
| 20 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘𝑧) ∈ V |
| 21 | | c0ex 11255 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
V |
| 22 | 20, 21 | ifex 4576 |
. . . . . . . . . . . . 13
⊢ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) ∈ V |
| 23 | 19, 9, 22 | fvmpt 7016 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ → (𝐺‘𝑧) = if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0)) |
| 24 | 23 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → (𝐺‘𝑧) = if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0)) |
| 25 | 24 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → ((𝐺‘𝑧) = 𝑦 ↔ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦)) |
| 26 | | eldifsni 4790 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (ran 𝐺 ∖ {0}) → 𝑦 ≠ 0) |
| 27 | 26 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → 𝑦 ≠ 0) |
| 28 | 27 | necomd 2996 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → 0 ≠
𝑦) |
| 29 | | iffalse 4534 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑧 ∈ 𝐴 → if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 0) |
| 30 | 29 | neeq1d 3000 |
. . . . . . . . . . . . 13
⊢ (¬
𝑧 ∈ 𝐴 → (if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) ≠ 𝑦 ↔ 0 ≠ 𝑦)) |
| 31 | 28, 30 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → (¬
𝑧 ∈ 𝐴 → if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) ≠ 𝑦)) |
| 32 | 31 | necon4bd 2960 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) →
(if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦 → 𝑧 ∈ 𝐴)) |
| 33 | 32 | pm4.71rd 562 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) →
(if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦 ↔ (𝑧 ∈ 𝐴 ∧ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦))) |
| 34 | 25, 33 | bitrd 279 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → ((𝐺‘𝑧) = 𝑦 ↔ (𝑧 ∈ 𝐴 ∧ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦))) |
| 35 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐴 → if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = (𝐹‘𝑧)) |
| 36 | 35 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐴 → (if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦 ↔ (𝐹‘𝑧) = 𝑦)) |
| 37 | 36 | pm5.32i 574 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐴 ∧ if(𝑧 ∈ 𝐴, (𝐹‘𝑧), 0) = 𝑦) ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) = 𝑦)) |
| 38 | 34, 37 | bitrdi 287 |
. . . . . . . 8
⊢ ((((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) ∧ 𝑧 ∈ ℝ) → ((𝐺‘𝑧) = 𝑦 ↔ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) = 𝑦))) |
| 39 | 38 | pm5.32da 579 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → ((𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦) ↔ (𝑧 ∈ ℝ ∧ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) = 𝑦)))) |
| 40 | | an12 645 |
. . . . . . 7
⊢ ((𝑧 ∈ ℝ ∧ (𝑧 ∈ 𝐴 ∧ (𝐹‘𝑧) = 𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦))) |
| 41 | 39, 40 | bitrdi 287 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → ((𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦) ↔ (𝑧 ∈ 𝐴 ∧ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦)))) |
| 42 | 10 | ffnd 6737 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐺 Fn
ℝ) |
| 43 | 42 | adantr 480 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → 𝐺 Fn ℝ) |
| 44 | | fniniseg 7080 |
. . . . . . 7
⊢ (𝐺 Fn ℝ → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
| 45 | 43, 44 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐺‘𝑧) = 𝑦))) |
| 46 | 3 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → 𝐹 Fn ℝ) |
| 47 | | fniniseg 7080 |
. . . . . . . 8
⊢ (𝐹 Fn ℝ → (𝑧 ∈ (◡𝐹 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦))) |
| 48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ (◡𝐹 “ {𝑦}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦))) |
| 49 | 48 | anbi2d 630 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → ((𝑧 ∈ 𝐴 ∧ 𝑧 ∈ (◡𝐹 “ {𝑦})) ↔ (𝑧 ∈ 𝐴 ∧ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = 𝑦)))) |
| 50 | 41, 45, 49 | 3bitr4d 311 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ (◡𝐹 “ {𝑦})))) |
| 51 | | elin 3967 |
. . . . 5
⊢ (𝑧 ∈ (𝐴 ∩ (◡𝐹 “ {𝑦})) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ (◡𝐹 “ {𝑦}))) |
| 52 | 50, 51 | bitr4di 289 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝑧 ∈ (◡𝐺 “ {𝑦}) ↔ 𝑧 ∈ (𝐴 ∩ (◡𝐹 “ {𝑦})))) |
| 53 | 52 | eqrdv 2735 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑦}) = (𝐴 ∩ (◡𝐹 “ {𝑦}))) |
| 54 | | simplr 769 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → 𝐴 ∈ dom
vol) |
| 55 | | i1fima 25713 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {𝑦}) ∈ dom vol) |
| 56 | 55 | ad2antrr 726 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (◡𝐹 “ {𝑦}) ∈ dom vol) |
| 57 | | inmbl 25577 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ (◡𝐹 “ {𝑦}) ∈ dom vol) → (𝐴 ∩ (◡𝐹 “ {𝑦})) ∈ dom vol) |
| 58 | 54, 56, 57 | syl2anc 584 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (𝐴 ∩ (◡𝐹 “ {𝑦})) ∈ dom vol) |
| 59 | 53, 58 | eqeltrd 2841 |
. 2
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑦}) ∈ dom vol) |
| 60 | 53 | fveq2d 6910 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑦})) = (vol‘(𝐴 ∩ (◡𝐹 “ {𝑦})))) |
| 61 | | mblvol 25565 |
. . . . 5
⊢ ((𝐴 ∩ (◡𝐹 “ {𝑦})) ∈ dom vol → (vol‘(𝐴 ∩ (◡𝐹 “ {𝑦}))) = (vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦})))) |
| 62 | 58, 61 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(𝐴 ∩ (◡𝐹 “ {𝑦}))) = (vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦})))) |
| 63 | 60, 62 | eqtrd 2777 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑦})) = (vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦})))) |
| 64 | | inss2 4238 |
. . . 4
⊢ (𝐴 ∩ (◡𝐹 “ {𝑦})) ⊆ (◡𝐹 “ {𝑦}) |
| 65 | | mblss 25566 |
. . . . 5
⊢ ((◡𝐹 “ {𝑦}) ∈ dom vol → (◡𝐹 “ {𝑦}) ⊆ ℝ) |
| 66 | 56, 65 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) → (◡𝐹 “ {𝑦}) ⊆ ℝ) |
| 67 | | mblvol 25565 |
. . . . . 6
⊢ ((◡𝐹 “ {𝑦}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑦})) = (vol*‘(◡𝐹 “ {𝑦}))) |
| 68 | 56, 67 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) = (vol*‘(◡𝐹 “ {𝑦}))) |
| 69 | | i1fima2sn 25715 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
| 70 | 69 | adantlr 715 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
| 71 | 68, 70 | eqeltrrd 2842 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol*‘(◡𝐹 “ {𝑦})) ∈ ℝ) |
| 72 | | ovolsscl 25521 |
. . . 4
⊢ (((𝐴 ∩ (◡𝐹 “ {𝑦})) ⊆ (◡𝐹 “ {𝑦}) ∧ (◡𝐹 “ {𝑦}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑦})) ∈ ℝ) → (vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦}))) ∈ ℝ) |
| 73 | 64, 66, 71, 72 | mp3an2i 1468 |
. . 3
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol*‘(𝐴 ∩ (◡𝐹 “ {𝑦}))) ∈ ℝ) |
| 74 | 63, 73 | eqeltrd 2841 |
. 2
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
∧ 𝑦 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑦})) ∈ ℝ) |
| 75 | 12, 16, 59, 74 | i1fd 25716 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐴 ∈ dom vol)
→ 𝐺 ∈ dom
∫1) |