| Step | Hyp | Ref
| Expression |
| 1 | | i1fadd.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
| 2 | | i1fadd.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
| 3 | 1, 2 | i1fadd 25730 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ dom
∫1) |
| 4 | | itg1add.4 |
. . . . . . 7
⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) |
| 5 | | ax-addf 11234 |
. . . . . . . . 9
⊢ +
:(ℂ × ℂ)⟶ℂ |
| 6 | | ffn 6736 |
. . . . . . . . 9
⊢ ( +
:(ℂ × ℂ)⟶ℂ → + Fn (ℂ ×
ℂ)) |
| 7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
⊢ + Fn
(ℂ × ℂ) |
| 8 | | i1frn 25712 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
| 9 | 1, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
| 10 | | i1frn 25712 |
. . . . . . . . . 10
⊢ (𝐺 ∈ dom ∫1
→ ran 𝐺 ∈
Fin) |
| 11 | 2, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
| 12 | | xpfi 9358 |
. . . . . . . . 9
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) |
| 13 | 9, 11, 12 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) |
| 14 | | resfnfinfin 9377 |
. . . . . . . 8
⊢ (( + Fn
(ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ∈ Fin) → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin) |
| 15 | 7, 13, 14 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin) |
| 16 | 4, 15 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Fin) |
| 17 | | rnfi 9380 |
. . . . . 6
⊢ (𝑃 ∈ Fin → ran 𝑃 ∈ Fin) |
| 18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝑃 ∈ Fin) |
| 19 | | difss 4136 |
. . . . 5
⊢ (ran
𝑃 ∖ {0}) ⊆ ran
𝑃 |
| 20 | | ssfi 9213 |
. . . . 5
⊢ ((ran
𝑃 ∈ Fin ∧ (ran
𝑃 ∖ {0}) ⊆ ran
𝑃) → (ran 𝑃 ∖ {0}) ∈
Fin) |
| 21 | 18, 19, 20 | sylancl 586 |
. . . 4
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin) |
| 22 | | ffun 6739 |
. . . . . . . . . . 11
⊢ ( +
:(ℂ × ℂ)⟶ℂ → Fun + ) |
| 23 | 5, 22 | ax-mp 5 |
. . . . . . . . . 10
⊢ Fun
+ |
| 24 | | i1ff 25711 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
| 25 | 1, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
| 26 | 25 | frnd 6744 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
| 27 | | ax-resscn 11212 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
| 28 | 26, 27 | sstrdi 3996 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
| 29 | | i1ff 25711 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
| 30 | 2, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
| 31 | 30 | frnd 6744 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐺 ⊆ ℝ) |
| 32 | 31, 27 | sstrdi 3996 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐺 ⊆ ℂ) |
| 33 | | xpss12 5700 |
. . . . . . . . . . . 12
⊢ ((ran
𝐹 ⊆ ℂ ∧ ran
𝐺 ⊆ ℂ) →
(ran 𝐹 × ran 𝐺) ⊆ (ℂ ×
ℂ)) |
| 34 | 28, 32, 33 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ ×
ℂ)) |
| 35 | 5 | fdmi 6747 |
. . . . . . . . . . 11
⊢ dom + =
(ℂ × ℂ) |
| 36 | 34, 35 | sseqtrrdi 4025 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + ) |
| 37 | | funfvima2 7251 |
. . . . . . . . . 10
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
| 38 | 23, 36, 37 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
| 39 | | opelxpi 5722 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → 〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺)) |
| 40 | 38, 39 | impel 505 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺))) |
| 41 | | df-ov 7434 |
. . . . . . . 8
⊢ (𝑥 + 𝑦) = ( + ‘〈𝑥, 𝑦〉) |
| 42 | 4 | rneqi 5948 |
. . . . . . . . 9
⊢ ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺)) |
| 43 | | df-ima 5698 |
. . . . . . . . 9
⊢ ( +
“ (ran 𝐹 × ran
𝐺)) = ran ( + ↾ (ran
𝐹 × ran 𝐺)) |
| 44 | 42, 43 | eqtr4i 2768 |
. . . . . . . 8
⊢ ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺)) |
| 45 | 40, 41, 44 | 3eltr4g 2858 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃) |
| 46 | 25 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn ℝ) |
| 47 | | dffn3 6748 |
. . . . . . . 8
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
| 48 | 46, 47 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
| 49 | 30 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Fn ℝ) |
| 50 | | dffn3 6748 |
. . . . . . . 8
⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺) |
| 51 | 49, 50 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺) |
| 52 | | reex 11246 |
. . . . . . . 8
⊢ ℝ
∈ V |
| 53 | 52 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
V) |
| 54 | | inidm 4227 |
. . . . . . 7
⊢ (ℝ
∩ ℝ) = ℝ |
| 55 | 45, 48, 51, 53, 53, 54 | off 7715 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘f + 𝐺):ℝ⟶ran 𝑃) |
| 56 | 55 | frnd 6744 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ran 𝑃) |
| 57 | 56 | ssdifd 4145 |
. . . 4
⊢ (𝜑 → (ran (𝐹 ∘f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0})) |
| 58 | 26 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ) |
| 59 | 31 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
| 60 | 58, 59 | anim12dan 619 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) |
| 61 | | readdcl 11238 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ) |
| 62 | 60, 61 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ) |
| 63 | 62 | ralrimivva 3202 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ) |
| 64 | | funimassov 7610 |
. . . . . . . 8
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(( + “ (ran 𝐹 ×
ran 𝐺)) ⊆ ℝ
↔ ∀𝑦 ∈ ran
𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)) |
| 65 | 23, 36, 64 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)) |
| 66 | 63, 65 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ) |
| 67 | 44, 66 | eqsstrid 4022 |
. . . . 5
⊢ (𝜑 → ran 𝑃 ⊆ ℝ) |
| 68 | 67 | ssdifd 4145 |
. . . 4
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖
{0})) |
| 69 | | itg1val2 25719 |
. . . 4
⊢ (((𝐹 ∘f + 𝐺) ∈ dom ∫1
∧ ((ran 𝑃 ∖ {0})
∈ Fin ∧ (ran (𝐹
∘f + 𝐺)
∖ {0}) ⊆ (ran 𝑃
∖ {0}) ∧ (ran 𝑃
∖ {0}) ⊆ (ℝ ∖ {0}))) →
(∫1‘(𝐹
∘f + 𝐺)) =
Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤})))) |
| 70 | 3, 21, 57, 68, 69 | syl13anc 1374 |
. . 3
⊢ (𝜑 →
(∫1‘(𝐹
∘f + 𝐺)) =
Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤})))) |
| 71 | 30 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ) |
| 72 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin) |
| 73 | | inss2 4238 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) |
| 74 | 73 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})) |
| 75 | | i1fima 25713 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol) |
| 76 | 1, 75 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol) |
| 77 | | i1fima 25713 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) |
| 78 | 2, 77 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) |
| 79 | | inmbl 25577 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
| 80 | 76, 78, 79 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
| 81 | 80 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
| 82 | 19, 67 | sstrid 3995 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆
ℝ) |
| 83 | 82 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ) |
| 84 | 83 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ) |
| 85 | 59 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
| 86 | 84, 85 | resubcld 11691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 − 𝑧) ∈ ℝ) |
| 87 | 84 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ) |
| 88 | 85 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ) |
| 89 | 87, 88 | npcand 11624 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) = 𝑤) |
| 90 | | eldifsni 4790 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0) |
| 91 | 90 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0) |
| 92 | 89, 91 | eqnetrd 3008 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) ≠ 0) |
| 93 | | oveq12 7440 |
. . . . . . . . . . . . 13
⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = (0 + 0)) |
| 94 | | 00id 11436 |
. . . . . . . . . . . . 13
⊢ (0 + 0) =
0 |
| 95 | 93, 94 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = 0) |
| 96 | 95 | necon3ai 2965 |
. . . . . . . . . . 11
⊢ (((𝑤 − 𝑧) + 𝑧) ≠ 0 → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) |
| 97 | 92, 96 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) |
| 98 | | itg1add.3 |
. . . . . . . . . . 11
⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) |
| 99 | 1, 2, 98 | itg1addlem3 25733 |
. . . . . . . . . 10
⊢ ((((𝑤 − 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
| 100 | 86, 85, 97, 99 | syl21anc 838 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
| 101 | 1, 2, 98 | itg1addlem2 25732 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
| 102 | 101 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
| 103 | 102, 86, 85 | fovcdmd 7605 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ) |
| 104 | 100, 103 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
| 105 | 71, 72, 74, 81, 104 | itg1addlem1 25727 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
| 106 | 83 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ) |
| 107 | 1, 2 | i1faddlem 25728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (◡(𝐹 ∘f + 𝐺) “ {𝑤}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
| 108 | 106, 107 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (◡(𝐹 ∘f + 𝐺) “ {𝑤}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
| 109 | 108 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤})) = (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
| 110 | 100 | sumeq2dv 15738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
| 111 | 105, 109,
110 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) |
| 112 | 111 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧))) |
| 113 | 103 | recnd 11289 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ) |
| 114 | 72, 106, 113 | fsummulc2 15820 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 115 | 112, 114 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 116 | 115 | sumeq2dv 15738 |
. . 3
⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 117 | 87, 113 | mulcld 11281 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
| 118 | 117 | anasss 466 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
| 119 | 21, 11, 118 | fsumcom 15811 |
. . 3
⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 120 | 70, 116, 119 | 3eqtrd 2781 |
. 2
⊢ (𝜑 →
(∫1‘(𝐹
∘f + 𝐺)) =
Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 121 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦 + 𝑧) = ((𝑤 − 𝑧) + 𝑧)) |
| 122 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦𝐼𝑧) = ((𝑤 − 𝑧)𝐼𝑧)) |
| 123 | 121, 122 | oveq12d 7449 |
. . . . . 6
⊢ (𝑦 = (𝑤 − 𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧))) |
| 124 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin) |
| 125 | 67 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ) |
| 126 | 125 | sselda 3983 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ) |
| 127 | 59 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ) |
| 128 | 126, 127 | resubcld 11691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣 − 𝑧) ∈ ℝ) |
| 129 | 128 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣 − 𝑧) ∈ ℝ)) |
| 130 | 126 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ) |
| 131 | 130 | adantrr 717 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ) |
| 132 | 67 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ) |
| 133 | 132 | ad2ant2rl 749 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ) |
| 134 | 133 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ) |
| 135 | 59 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ) |
| 136 | 135 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ) |
| 137 | 131, 134,
136 | subcan2ad 11665 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦)) |
| 138 | 137 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦))) |
| 139 | 129, 138 | dom2lem 9032 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ) |
| 140 | | f1f1orn 6859 |
. . . . . . 7
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
| 141 | 139, 140 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
| 142 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑣 = 𝑤 → (𝑣 − 𝑧) = (𝑤 − 𝑧)) |
| 143 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) |
| 144 | | ovex 7464 |
. . . . . . . 8
⊢ (𝑤 − 𝑧) ∈ V |
| 145 | 142, 143,
144 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧)) |
| 146 | 145 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧)) |
| 147 | | f1f 6804 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ) |
| 148 | | frn 6743 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ) |
| 149 | 139, 147,
148 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ) |
| 150 | 149 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑦 ∈ ℝ) |
| 151 | 59 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑧 ∈ ℝ) |
| 152 | 150, 151 | readdcld 11290 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦 + 𝑧) ∈ ℝ) |
| 153 | 101 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
| 154 | 153, 150,
151 | fovcdmd 7605 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦𝐼𝑧) ∈ ℝ) |
| 155 | 152, 154 | remulcld 11291 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ) |
| 156 | 155 | recnd 11289 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
| 157 | 123, 124,
141, 146, 156 | fsumf1o 15759 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧))) |
| 158 | 125 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ) |
| 159 | 158 | recnd 11289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ) |
| 160 | 135 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ) |
| 161 | 159, 160 | npcand 11624 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤 − 𝑧) + 𝑧) = 𝑤) |
| 162 | 161 | oveq1d 7446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = (𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 163 | 162 | sumeq2dv 15738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 164 | 157, 163 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 165 | 36 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + ) |
| 166 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
| 167 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺) |
| 168 | 166, 167 | opelxpd 5724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺)) |
| 169 | | funfvima2 7251 |
. . . . . . . . . . . 12
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
| 170 | 23, 169 | mpan 690 |
. . . . . . . . . . 11
⊢ ((ran
𝐹 × ran 𝐺) ⊆ dom + →
(〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
| 171 | 165, 168,
170 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺))) |
| 172 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑦 + 𝑧) = ( + ‘〈𝑦, 𝑧〉) |
| 173 | 171, 172,
44 | 3eltr4g 2858 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃) |
| 174 | 58 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ) |
| 175 | 174 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ) |
| 176 | 135 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ) |
| 177 | 175, 176 | pncand 11621 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦) |
| 178 | 177 | eqcomd 2743 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧)) |
| 179 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑦 + 𝑧) → (𝑣 − 𝑧) = ((𝑦 + 𝑧) − 𝑧)) |
| 180 | 179 | rspceeqv 3645 |
. . . . . . . . 9
⊢ (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
| 181 | 173, 178,
180 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
| 182 | 181 | ralrimiva 3146 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
| 183 | | ssabral 4065 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} ↔ ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
| 184 | 182, 183 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)}) |
| 185 | 143 | rnmpt 5968 |
. . . . . 6
⊢ ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} |
| 186 | 184, 185 | sseqtrrdi 4025 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
| 187 | 59 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ) |
| 188 | 174, 187 | readdcld 11290 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ) |
| 189 | 101 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
| 190 | 189, 174,
187 | fovcdmd 7605 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ) |
| 191 | 188, 190 | remulcld 11291 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ) |
| 192 | 191 | recnd 11289 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
| 193 | 149 | ssdifd 4145 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹)) |
| 194 | 193 | sselda 3983 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹)) |
| 195 | | eldifi 4131 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (ℝ ∖ ran
𝐹) → 𝑦 ∈
ℝ) |
| 196 | 195 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ) |
| 197 | 59 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ) |
| 198 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0)) |
| 199 | 1, 2, 98 | itg1addlem3 25733 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬
(𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})))) |
| 200 | 196, 197,
198, 199 | syl21anc 838 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})))) |
| 201 | | inss1 4237 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {𝑦}) |
| 202 | | eldifn 4132 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (ℝ ∖ ran
𝐹) → ¬ 𝑦 ∈ ran 𝐹) |
| 203 | 202 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹) |
| 204 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑣 ∈ V |
| 205 | 204 | eliniseg 6112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ V → (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)) |
| 206 | 205 | elv 3485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦) |
| 207 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
| 208 | 204, 207 | brelrn 5953 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣𝐹𝑦 → 𝑦 ∈ ran 𝐹) |
| 209 | 206, 208 | sylbi 217 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ (◡𝐹 “ {𝑦}) → 𝑦 ∈ ran 𝐹) |
| 210 | 203, 209 | nsyl 140 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑣 ∈ (◡𝐹 “ {𝑦})) |
| 211 | 210 | pm2.21d 121 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑣 ∈ (◡𝐹 “ {𝑦}) → 𝑣 ∈ ∅)) |
| 212 | 211 | ssrdv 3989 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (◡𝐹 “ {𝑦}) ⊆ ∅) |
| 213 | 201, 212 | sstrid 3995 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅) |
| 214 | | ss0 4402 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅ → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅) |
| 215 | 213, 214 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅) |
| 216 | 215 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = (vol‘∅)) |
| 217 | | 0mbl 25574 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ dom vol |
| 218 | | mblvol 25565 |
. . . . . . . . . . . . . 14
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
| 219 | 217, 218 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(vol‘∅) = (vol*‘∅) |
| 220 | | ovol0 25528 |
. . . . . . . . . . . . 13
⊢
(vol*‘∅) = 0 |
| 221 | 219, 220 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
(vol‘∅) = 0 |
| 222 | 216, 221 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = 0) |
| 223 | 200, 222 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0) |
| 224 | 223 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0)) |
| 225 | 196, 197 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ) |
| 226 | 225 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ) |
| 227 | 226 | mul01d 11460 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0) |
| 228 | 224, 227 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
| 229 | 228 | expr 456 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)) |
| 230 | | oveq12 7440 |
. . . . . . . . . 10
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0)) |
| 231 | 230, 94 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0) |
| 232 | | oveq12 7440 |
. . . . . . . . . 10
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0)) |
| 233 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 234 | | iftrue 4531 |
. . . . . . . . . . . 12
⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) = 0) |
| 235 | | c0ex 11255 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
| 236 | 234, 98, 235 | ovmpoa 7588 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0) |
| 237 | 233, 233,
236 | mp2an 692 |
. . . . . . . . . 10
⊢ (0𝐼0) = 0 |
| 238 | 232, 237 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0) |
| 239 | 231, 238 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0)) |
| 240 | | 0cn 11253 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
| 241 | 240 | mul01i 11451 |
. . . . . . . 8
⊢ (0
· 0) = 0 |
| 242 | 239, 241 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
| 243 | 229, 242 | pm2.61d2 181 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
| 244 | 194, 243 | syldan 591 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
| 245 | | f1ofo 6855 |
. . . . . . 7
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
| 246 | 141, 245 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
| 247 | | fofi 9351 |
. . . . . 6
⊢ ((ran
𝑃 ∈ Fin ∧ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin) |
| 248 | 124, 246,
247 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin) |
| 249 | 186, 192,
244, 248 | fsumss 15761 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |
| 250 | 19 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) |
| 251 | 117 | an32s 652 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
| 252 | | dfin4 4278 |
. . . . . . . 8
⊢ (ran
𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) |
| 253 | | inss2 4238 |
. . . . . . . 8
⊢ (ran
𝑃 ∩ {0}) ⊆
{0} |
| 254 | 252, 253 | eqsstrri 4031 |
. . . . . . 7
⊢ (ran
𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆
{0} |
| 255 | 254 | sseli 3979 |
. . . . . 6
⊢ (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0}) |
| 256 | | elsni 4643 |
. . . . . . . . 9
⊢ (𝑤 ∈ {0} → 𝑤 = 0) |
| 257 | 256 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0) |
| 258 | 257 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = (0 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 259 | 101 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
| 260 | 257, 233 | eqeltrdi 2849 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ) |
| 261 | 59 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ) |
| 262 | 260, 261 | resubcld 11691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 − 𝑧) ∈ ℝ) |
| 263 | 259, 262,
261 | fovcdmd 7605 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ) |
| 264 | 263 | recnd 11289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ) |
| 265 | 264 | mul02d 11459 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
| 266 | 258, 265 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
| 267 | 255, 266 | sylan2 593 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
| 268 | 250, 251,
267, 124 | fsumss 15761 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 269 | 164, 249,
268 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 270 | 269 | sumeq2dv 15738 |
. 2
⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
| 271 | 192 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
| 272 | 11, 9, 271 | fsumcom 15811 |
. 2
⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |
| 273 | 120, 270,
272 | 3eqtr2d 2783 |
1
⊢ (𝜑 →
(∫1‘(𝐹
∘f + 𝐺)) =
Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |