| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | readdcl 11239 | . . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) | 
| 2 | 1 | adantl 481 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ) | 
| 3 |  | i1fadd.1 | . . . 4
⊢ (𝜑 → 𝐹 ∈ dom
∫1) | 
| 4 |  | i1ff 25712 | . . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) | 
| 5 | 3, 4 | syl 17 | . . 3
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 6 |  | i1fadd.2 | . . . 4
⊢ (𝜑 → 𝐺 ∈ dom
∫1) | 
| 7 |  | i1ff 25712 | . . . 4
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) | 
| 8 | 6, 7 | syl 17 | . . 3
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) | 
| 9 |  | reex 11247 | . . . 4
⊢ ℝ
∈ V | 
| 10 | 9 | a1i 11 | . . 3
⊢ (𝜑 → ℝ ∈
V) | 
| 11 |  | inidm 4226 | . . 3
⊢ (ℝ
∩ ℝ) = ℝ | 
| 12 | 2, 5, 8, 10, 10, 11 | off 7716 | . 2
⊢ (𝜑 → (𝐹 ∘f + 𝐺):ℝ⟶ℝ) | 
| 13 |  | i1frn 25713 | . . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) | 
| 14 | 3, 13 | syl 17 | . . . . 5
⊢ (𝜑 → ran 𝐹 ∈ Fin) | 
| 15 |  | i1frn 25713 | . . . . . 6
⊢ (𝐺 ∈ dom ∫1
→ ran 𝐺 ∈
Fin) | 
| 16 | 6, 15 | syl 17 | . . . . 5
⊢ (𝜑 → ran 𝐺 ∈ Fin) | 
| 17 |  | xpfi 9359 | . . . . 5
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) | 
| 18 | 14, 16, 17 | syl2anc 584 | . . . 4
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) | 
| 19 |  | eqid 2736 | . . . . . 6
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) = (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) | 
| 20 |  | ovex 7465 | . . . . . 6
⊢ (𝑢 + 𝑣) ∈ V | 
| 21 | 19, 20 | fnmpoi 8096 | . . . . 5
⊢ (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) Fn (ran 𝐹 × ran 𝐺) | 
| 22 |  | dffn4 6825 | . . . . 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 9352 | . . . 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 2736 | . . . . . . . . 9
⊢ (𝑥 + 𝑦) = (𝑥 + 𝑦) | 
| 27 |  | rspceov 7481 | . . . . . . . . 9
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ∧ (𝑥 + 𝑦) = (𝑥 + 𝑦)) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣)) | 
| 28 | 26, 27 | mp3an3 1451 | . . . . . . . 8
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣)) | 
| 29 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑥 + 𝑦) ∈ V | 
| 30 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑤 = (𝑥 + 𝑦) → (𝑤 = (𝑢 + 𝑣) ↔ (𝑥 + 𝑦) = (𝑢 + 𝑣))) | 
| 31 | 30 | 2rexbidv 3221 | . . . . . . . . 9
⊢ (𝑤 = (𝑥 + 𝑦) → (∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣) ↔ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺(𝑥 + 𝑦) = (𝑢 + 𝑣))) | 
| 32 | 29, 31 | elab 3678 | . . . . . . . 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 6736 | . . . . . . 7
⊢ (𝜑 → 𝐹 Fn ℝ) | 
| 36 |  | dffn3 6747 | . . . . . . 7
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) | 
| 37 | 35, 36 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) | 
| 38 | 8 | ffnd 6736 | . . . . . . 7
⊢ (𝜑 → 𝐺 Fn ℝ) | 
| 39 |  | dffn3 6747 | . . . . . . 7
⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺) | 
| 40 | 38, 39 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺) | 
| 41 | 34, 37, 40, 10, 10, 11 | off 7716 | . . . . 5
⊢ (𝜑 → (𝐹 ∘f + 𝐺):ℝ⟶{𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) | 
| 42 | 41 | frnd 6743 | . . . 4
⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)}) | 
| 43 | 19 | rnmpo 7567 | . . . 4
⊢ ran
(𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣)) = {𝑤 ∣ ∃𝑢 ∈ ran 𝐹∃𝑣 ∈ ran 𝐺 𝑤 = (𝑢 + 𝑣)} | 
| 44 | 42, 43 | sseqtrrdi 4024 | . . 3
⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ran (𝑢 ∈ ran 𝐹, 𝑣 ∈ ran 𝐺 ↦ (𝑢 + 𝑣))) | 
| 45 | 25, 44 | ssfid 9302 | . 2
⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ∈ Fin) | 
| 46 | 12 | frnd 6743 | . . . . . . 7
⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ℝ) | 
| 47 | 46 | ssdifssd 4146 | . . . . . 6
⊢ (𝜑 → (ran (𝐹 ∘f + 𝐺) ∖ {0}) ⊆
ℝ) | 
| 48 | 47 | sselda 3982 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → 𝑦 ∈ ℝ) | 
| 49 | 48 | recnd 11290 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → 𝑦 ∈ ℂ) | 
| 50 | 3, 6 | i1faddlem 25729 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (◡(𝐹 ∘f + 𝐺) “ {𝑦}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) | 
| 51 | 49, 50 | syldan 591 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (◡(𝐹 ∘f + 𝐺) “ {𝑦}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) | 
| 52 | 16 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → ran 𝐺 ∈ Fin) | 
| 53 | 3 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹 ∈ dom
∫1) | 
| 54 |  | i1fmbf 25711 | . . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
MblFn) | 
| 55 | 53, 54 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹 ∈ MblFn) | 
| 56 | 5 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐹:ℝ⟶ℝ) | 
| 57 | 12 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝐹 ∘f + 𝐺):ℝ⟶ℝ) | 
| 58 | 57 | frnd 6743 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ran (𝐹 ∘f + 𝐺) ⊆ ℝ) | 
| 59 |  | eldifi 4130 | . . . . . . . . . 10
⊢ (𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0}) → 𝑦 ∈ ran (𝐹 ∘f + 𝐺)) | 
| 60 | 59 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑦 ∈ ran (𝐹 ∘f + 𝐺)) | 
| 61 | 58, 60 | sseldd 3983 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑦 ∈ ℝ) | 
| 62 | 8 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → 𝐺:ℝ⟶ℝ) | 
| 63 | 62 | frnd 6743 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → ran 𝐺 ⊆ ℝ) | 
| 64 | 63 | sselda 3982 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) | 
| 65 | 61, 64 | resubcld 11692 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑦 − 𝑧) ∈ ℝ) | 
| 66 |  | mbfimasn 25668 | . . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧
(𝑦 − 𝑧) ∈ ℝ) → (◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol) | 
| 67 | 55, 56, 65, 66 | syl3anc 1372 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol) | 
| 68 | 6 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺 ∈ dom
∫1) | 
| 69 |  | i1fmbf 25711 | . . . . . . . 8
⊢ (𝐺 ∈ dom ∫1
→ 𝐺 ∈
MblFn) | 
| 70 | 68, 69 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺 ∈ MblFn) | 
| 71 | 8 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐺:ℝ⟶ℝ) | 
| 72 |  | mbfimasn 25668 | . . . . . . 7
⊢ ((𝐺 ∈ MblFn ∧ 𝐺:ℝ⟶ℝ ∧
𝑧 ∈ ℝ) →
(◡𝐺 “ {𝑧}) ∈ dom vol) | 
| 73 | 70, 71, 64, 72 | syl3anc 1372 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (◡𝐺 “ {𝑧}) ∈ dom vol) | 
| 74 |  | inmbl 25578 | . . . . . 6
⊢ (((◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) | 
| 75 | 67, 73, 74 | syl2anc 584 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) | 
| 76 | 75 | ralrimiva 3145 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → ∀𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) | 
| 77 |  | finiunmbl 25580 | . . . 4
⊢ ((ran
𝐺 ∈ Fin ∧
∀𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) → ∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) | 
| 78 | 52, 76, 77 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → ∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) | 
| 79 | 51, 78 | eqeltrd 2840 | . 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (◡(𝐹 ∘f + 𝐺) “ {𝑦}) ∈ dom vol) | 
| 80 |  | mblvol 25566 | . . . 4
⊢ ((◡(𝐹 ∘f + 𝐺) “ {𝑦}) ∈ dom vol → (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘f + 𝐺) “ {𝑦}))) | 
| 81 | 79, 80 | syl 17 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑦})) = (vol*‘(◡(𝐹 ∘f + 𝐺) “ {𝑦}))) | 
| 82 |  | mblss 25567 | . . . . 5
⊢ ((◡(𝐹 ∘f + 𝐺) “ {𝑦}) ∈ dom vol → (◡(𝐹 ∘f + 𝐺) “ {𝑦}) ⊆ ℝ) | 
| 83 | 79, 82 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (◡(𝐹 ∘f + 𝐺) “ {𝑦}) ⊆ ℝ) | 
| 84 |  | inss1 4236 | . . . . . . . 8
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {(𝑦 − 𝑧)}) | 
| 85 | 67 | adantrr 717 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol) | 
| 86 |  | mblss 25567 | . . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol → (◡𝐹 “ {(𝑦 − 𝑧)}) ⊆ ℝ) | 
| 87 | 85, 86 | syl 17 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (◡𝐹 “ {(𝑦 − 𝑧)}) ⊆ ℝ) | 
| 88 |  | mblvol 25566 | . . . . . . . . . 10
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∈ dom vol → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) = (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)}))) | 
| 89 | 85, 88 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) = (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)}))) | 
| 90 |  | simprr 772 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → 𝑧 = 0) | 
| 91 | 90 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (𝑦 − 𝑧) = (𝑦 − 0)) | 
| 92 | 49 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → 𝑦 ∈ ℂ) | 
| 93 | 92 | subid1d 11610 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (𝑦 − 0) = 𝑦) | 
| 94 | 91, 93 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (𝑦 − 𝑧) = 𝑦) | 
| 95 | 94 | sneqd 4637 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → {(𝑦 − 𝑧)} = {𝑦}) | 
| 96 | 95 | imaeq2d 6077 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (◡𝐹 “ {(𝑦 − 𝑧)}) = (◡𝐹 “ {𝑦})) | 
| 97 | 96 | fveq2d 6909 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) = (vol‘(◡𝐹 “ {𝑦}))) | 
| 98 |  | i1fima2sn 25716 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) →
(vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) | 
| 99 | 3, 98 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) | 
| 100 | 99 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {𝑦})) ∈ ℝ) | 
| 101 | 97, 100 | eqeltrd 2840 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol‘(◡𝐹 “ {(𝑦 − 𝑧)})) ∈ ℝ) | 
| 102 | 89, 101 | eqeltrrd 2841 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)})) ∈ ℝ) | 
| 103 |  | ovolsscl 25522 | . . . . . . . 8
⊢ ((((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {(𝑦 − 𝑧)}) ∧ (◡𝐹 “ {(𝑦 − 𝑧)}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {(𝑦 − 𝑧)})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) | 
| 104 | 84, 87, 102, 103 | mp3an2i 1467 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0)) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) | 
| 105 | 104 | expr 456 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑧 = 0 → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) | 
| 106 |  | eldifsn 4785 | . . . . . . . 8
⊢ (𝑧 ∈ (ran 𝐺 ∖ {0}) ↔ (𝑧 ∈ ran 𝐺 ∧ 𝑧 ≠ 0)) | 
| 107 |  | inss2 4237 | . . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) | 
| 108 |  | eldifi 4130 | . . . . . . . . . 10
⊢ (𝑧 ∈ (ran 𝐺 ∖ {0}) → 𝑧 ∈ ran 𝐺) | 
| 109 |  | mblss 25567 | . . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (◡𝐺 “ {𝑧}) ⊆ ℝ) | 
| 110 | 73, 109 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (◡𝐺 “ {𝑧}) ⊆ ℝ) | 
| 111 | 108, 110 | sylan2 593 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ⊆ ℝ) | 
| 112 |  | i1fima 25714 | . . . . . . . . . . . . 13
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) | 
| 113 | 6, 112 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) | 
| 114 | 113 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (◡𝐺 “ {𝑧}) ∈ dom vol) | 
| 115 |  | mblvol 25566 | . . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑧}) ∈ dom vol → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) | 
| 116 | 114, 115 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) = (vol*‘(◡𝐺 “ {𝑧}))) | 
| 117 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → 𝐺 ∈ dom
∫1) | 
| 118 |  | i1fima2sn 25716 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) →
(vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) | 
| 119 | 117, 118 | sylan 580 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol‘(◡𝐺 “ {𝑧})) ∈ ℝ) | 
| 120 | 116, 119 | eqeltrrd 2841 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) | 
| 121 |  | ovolsscl 25522 | . . . . . . . . 9
⊢ ((((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) ∧ (◡𝐺 “ {𝑧}) ⊆ ℝ ∧ (vol*‘(◡𝐺 “ {𝑧})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) | 
| 122 | 107, 111,
120, 121 | mp3an2i 1467 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ (ran 𝐺 ∖ {0})) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) | 
| 123 | 106, 122 | sylan2br 595 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑧 ≠ 0)) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) | 
| 124 | 123 | expr 456 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑧 ≠ 0 → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) | 
| 125 | 105, 124 | pm2.61dne 3027 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) | 
| 126 | 52, 125 | fsumrecl 15771 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) | 
| 127 | 51 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (vol*‘(◡(𝐹 ∘f + 𝐺) “ {𝑦})) = (vol*‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) | 
| 128 | 107, 110 | sstrid 3994 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ) | 
| 129 | 128, 125 | jca 511 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) | 
| 130 | 129 | ralrimiva 3145 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → ∀𝑧 ∈ ran 𝐺(((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) | 
| 131 |  | ovolfiniun 25537 | . . . . . 6
⊢ ((ran
𝐺 ∈ Fin ∧
∀𝑧 ∈ ran 𝐺(((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ ℝ ∧ (vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)) →
(vol*‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) | 
| 132 | 52, 130, 131 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (vol*‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) | 
| 133 | 127, 132 | eqbrtrd 5164 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (vol*‘(◡(𝐹 ∘f + 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) | 
| 134 |  | ovollecl 25519 | . . . 4
⊢ (((◡(𝐹 ∘f + 𝐺) “ {𝑦}) ⊆ ℝ ∧ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ ∧ (vol*‘(◡(𝐹 ∘f + 𝐺) “ {𝑦})) ≤ Σ𝑧 ∈ ran 𝐺(vol*‘((◡𝐹 “ {(𝑦 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) → (vol*‘(◡(𝐹 ∘f + 𝐺) “ {𝑦})) ∈ ℝ) | 
| 135 | 83, 126, 133, 134 | syl3anc 1372 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (vol*‘(◡(𝐹 ∘f + 𝐺) “ {𝑦})) ∈ ℝ) | 
| 136 | 81, 135 | eqeltrd 2840 | . 2
⊢ ((𝜑 ∧ 𝑦 ∈ (ran (𝐹 ∘f + 𝐺) ∖ {0})) → (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑦})) ∈ ℝ) | 
| 137 | 12, 45, 79, 136 | i1fd 25717 | 1
⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ dom
∫1) |