| Step | Hyp | Ref
| Expression |
| 1 | | remulcl 11240 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
| 2 | 1 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
| 3 | | i1fadd.1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
| 4 | | i1ff 25711 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
| 5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
| 6 | | i1fadd.2 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
| 7 | | i1ff 25711 |
. . . 4
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
| 8 | 6, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
| 9 | | reex 11246 |
. . . 4
⊢ ℝ
∈ V |
| 10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ∈
V) |
| 11 | | inidm 4227 |
. . 3
⊢ (ℝ
∩ ℝ) = ℝ |
| 12 | 2, 5, 8, 10, 10, 11 | off 7715 |
. 2
⊢ (𝜑 → (𝐹 ∘f · 𝐺):ℝ⟶ℝ) |
| 13 | | i1frn 25712 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
| 14 | 3, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
| 15 | | i1frn 25712 |
. . . . . 6
⊢ (𝐺 ∈ dom ∫1
→ ran 𝐺 ∈
Fin) |
| 16 | 6, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
| 17 | | xpfi 9358 |
. . . . 5
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) |
| 18 | 14, 16, 17 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) |
| 19 | | eqid 2737 |
. . . . . 6
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) = (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) |
| 20 | | ovex 7464 |
. . . . . 6
⊢ (𝑢 · 𝑣) ∈ V |
| 21 | 19, 20 | fnmpoi 8095 |
. . . . 5
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) Fn (ran 𝐹 × ran 𝐺) |
| 22 | | dffn4 6826 |
. . . . 5
⊢ ((𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) Fn (ran 𝐹 × ran 𝐺) ↔ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣))) |
| 23 | 21, 22 | mpbi 230 |
. . . 4
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) |
| 24 | | fofi 9351 |
. . . 4
⊢ (((ran
𝐹 × ran 𝐺) ∈ Fin ∧ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)):(ran 𝐹 × ran 𝐺)–onto→ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣))) → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) ∈ Fin) |
| 25 | 18, 23, 24 | sylancl 586 |
. . 3
⊢ (𝜑 → ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) ∈ Fin) |
| 26 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 · 𝑦) = (𝑥 · 𝑦) |
| 27 | | rspceov 7480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ∧ (𝑥 · 𝑦) = (𝑥 · 𝑦)) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 · 𝑦) = (𝑢 · 𝑣)) |
| 28 | 26, 27 | mp3an3 1452 |
. . . . . . . 8
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 · 𝑦) = (𝑢 · 𝑣)) |
| 29 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑥 · 𝑦) ∈ V |
| 30 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 · 𝑦) → (𝑤 = (𝑢 · 𝑣) ↔ (𝑥 · 𝑦) = (𝑢 · 𝑣))) |
| 31 | 30 | 2rexbidv 3222 |
. . . . . . . . 9
⊢ (𝑤 = (𝑥 · 𝑦) → (∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣) ↔ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 · 𝑦) = (𝑢 · 𝑣))) |
| 32 | 29, 31 | elab 3679 |
. . . . . . . 8
⊢ ((𝑥 · 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣)} ↔ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 · 𝑦) = (𝑢 · 𝑣)) |
| 33 | 28, 32 | sylibr 234 |
. . . . . . 7
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → (𝑥 · 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣)}) |
| 34 | 33 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 · 𝑦) ∈ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣)}) |
| 35 | 5 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn ℝ) |
| 36 | | dffn3 6748 |
. . . . . . 7
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
| 37 | 35, 36 | sylib 218 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
| 38 | 8 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn ℝ) |
| 39 | | dffn3 6748 |
. . . . . . 7
⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺) |
| 40 | 38, 39 | sylib 218 |
. . . . . 6
⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺) |
| 41 | 34, 37, 40, 10, 10, 11 | off 7715 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘f · 𝐺):ℝ⟶{𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣)}) |
| 42 | 41 | frnd 6744 |
. . . 4
⊢ (𝜑 → ran (𝐹 ∘f · 𝐺) ⊆ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣)}) |
| 43 | 19 | rnmpo 7566 |
. . . 4
⊢ ran
(𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣)) = {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 · 𝑣)} |
| 44 | 42, 43 | sseqtrrdi 4025 |
. . 3
⊢ (𝜑 → ran (𝐹 ∘f · 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 · 𝑣))) |
| 45 | 25, 44 | ssfid 9301 |
. 2
⊢ (𝜑 → ran (𝐹 ∘f · 𝐺) ∈ Fin) |
| 46 | 12 | frnd 6744 |
. . . . . . 7
⊢ (𝜑 → ran (𝐹 ∘f · 𝐺) ⊆
ℝ) |
| 47 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 48 | 46, 47 | sstrdi 3996 |
. . . . . 6
⊢ (𝜑 → ran (𝐹 ∘f · 𝐺) ⊆
ℂ) |
| 49 | 48 | ssdifd 4145 |
. . . . 5
⊢ (𝜑 → (ran (𝐹 ∘f · 𝐺) ∖ {0}) ⊆ (ℂ
∖ {0})) |
| 50 | 49 | sselda 3983 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) → 𝑦 ∈ (ℂ ∖
{0})) |
| 51 | 3, 6 | i1fmullem 25729 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {0})) → (◡(𝐹 ∘f · 𝐺) “ {𝑦}) = ∪
𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
| 52 | 50, 51 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) → (◡(𝐹 ∘f · 𝐺) “ {𝑦}) = ∪
𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
| 53 | | difss 4136 |
. . . . . 6
⊢ (ran
𝐺 ∖ {0}) ⊆ ran
𝐺 |
| 54 | | ssfi 9213 |
. . . . . 6
⊢ ((ran
𝐺 ∈ Fin ∧ (ran
𝐺 ∖ {0}) ⊆ ran
𝐺) → (ran 𝐺 ∖ {0}) ∈
Fin) |
| 55 | 16, 53, 54 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (ran 𝐺 ∖ {0}) ∈ Fin) |
| 56 | | i1fima 25713 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑦 / 𝑧)}) ∈ dom vol) |
| 57 | 3, 56 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ {(𝑦 / 𝑧)}) ∈ dom vol) |
| 58 | | i1fima 25713 |
. . . . . . . 8
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) |
| 59 | 6, 58 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) |
| 60 | | inmbl 25577 |
. . . . . . 7
⊢ (((◡𝐹 “ {(𝑦 / 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
| 61 | 57, 59, 60 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
| 62 | 61 | ralrimivw 3150 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
| 63 | | finiunmbl 25579 |
. . . . 5
⊢ (((ran
𝐺 ∖ {0}) ∈ Fin
∧ ∀𝑧 ∈ (ran
𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) → ∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
| 64 | 55, 62, 63 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
| 65 | 64 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) → ∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
| 66 | 52, 65 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) → (◡(𝐹 ∘f · 𝐺) “ {𝑦}) ∈ dom vol) |
| 67 | | mblvol 25565 |
. . . 4
⊢ ((◡(𝐹 ∘f · 𝐺) “ {𝑦}) ∈ dom vol → (vol‘(◡(𝐹 ∘f · 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘f · 𝐺) “ {𝑦}))) |
| 68 | 66, 67 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘f · 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘f · 𝐺) “ {𝑦}))) |
| 69 | | mblss 25566 |
. . . . 5
⊢ ((◡(𝐹 ∘f · 𝐺) “ {𝑦}) ∈ dom vol → (◡(𝐹 ∘f · 𝐺) “ {𝑦}) ⊆ ℝ) |
| 70 | 66, 69 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) → (◡(𝐹 ∘f · 𝐺) “ {𝑦}) ⊆ ℝ) |
| 71 | 55 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) → (ran
𝐺 ∖ {0}) ∈
Fin) |
| 72 | | inss2 4238 |
. . . . . . 7
⊢ ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) |
| 73 | 72 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})) |
| 74 | 59 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ∈ dom vol) |
| 75 | | mblss 25566 |
. . . . . . 7
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
| 76 | 74, 75 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ⊆ ℝ) |
| 77 | | mblvol 25565 |
. . . . . . . 8
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
| 78 | 74, 77 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) |
| 79 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) → 𝐺 ∈ dom
∫1) |
| 80 | | i1fima2sn 25715 |
. . . . . . . 8
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
| 81 | 79, 80 | sylan 580 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
| 82 | 78, 81 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) |
| 83 | | ovolsscl 25521 |
. . . . . 6
⊢ ((((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) ∧ (◡𝐺 “ {𝑧}) ⊆ ℝ ∧ (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
| 84 | 73, 76, 82, 83 | syl3anc 1373 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
| 85 | 71, 84 | fsumrecl 15770 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) →
Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
| 86 | 52 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘f · 𝐺) “ {𝑦})) = (vol*‘∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
| 87 | | mblss 25566 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
| 88 | 61, 87 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
| 89 | 88 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → ((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) |
| 90 | 89, 84 | jca 511 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
| 91 | 90 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) →
∀𝑧 ∈ (ran 𝐺 ∖ {0})(((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) |
| 92 | | ovolfiniun 25536 |
. . . . . 6
⊢ (((ran
𝐺 ∖ {0}) ∈ Fin
∧ ∀𝑧 ∈ (ran
𝐺 ∖ {0})(((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) →
(vol*‘∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
| 93 | 71, 91, 92 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) →
(vol*‘∪ 𝑧 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
| 94 | 86, 93 | eqbrtrd 5165 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘f · 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
| 95 | | ovollecl 25518 |
. . . 4
⊢ (((◡(𝐹 ∘f · 𝐺) “ {𝑦}) ⊆ ℝ ∧ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ ∧ (vol*‘(◡(𝐹 ∘f · 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ (ran 𝐺 ∖ {0})(vol*‘((◡𝐹 “ {(𝑦 / 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) → (vol*‘(◡(𝐹 ∘f · 𝐺) “ {𝑦})) ∈ ℝ) |
| 96 | 70, 85, 94, 95 | syl3anc 1373 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) →
(vol*‘(◡(𝐹 ∘f · 𝐺) “ {𝑦})) ∈ ℝ) |
| 97 | 68, 96 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f · 𝐺) ∖ {0})) →
(vol‘(◡(𝐹 ∘f · 𝐺) “ {𝑦})) ∈ ℝ) |
| 98 | 12, 45, 66, 97 | i1fd 25716 |
1
⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ dom
∫1) |