Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
2 | | i1fadd.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
3 | 1, 2 | i1fadd 23268 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ dom
∫1) |
4 | | i1frn 23250 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
6 | | i1frn 23250 |
. . . . . . . 8
⊢ (𝐺 ∈ dom ∫1
→ ran 𝐺 ∈
Fin) |
7 | 2, 6 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
8 | | xpfi 8116 |
. . . . . . 7
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) |
9 | 5, 7, 8 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) |
10 | | ax-addf 9894 |
. . . . . . . . . 10
⊢ +
:(ℂ × ℂ)⟶ℂ |
11 | | ffn 5958 |
. . . . . . . . . 10
⊢ ( +
:(ℂ × ℂ)⟶ℂ → + Fn (ℂ ×
ℂ)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢ + Fn
(ℂ × ℂ) |
13 | | i1ff 23249 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
14 | 1, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
15 | | frn 5966 |
. . . . . . . . . . . 12
⊢ (𝐹:ℝ⟶ℝ →
ran 𝐹 ⊆
ℝ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
17 | | ax-resscn 9872 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
18 | 16, 17 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
19 | | i1ff 23249 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
20 | 2, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
21 | | frn 5966 |
. . . . . . . . . . . 12
⊢ (𝐺:ℝ⟶ℝ →
ran 𝐺 ⊆
ℝ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐺 ⊆ ℝ) |
23 | 22, 17 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝐺 ⊆ ℂ) |
24 | | xpss12 5148 |
. . . . . . . . . 10
⊢ ((ran
𝐹 ⊆ ℂ ∧ ran
𝐺 ⊆ ℂ) →
(ran 𝐹 × ran 𝐺) ⊆ (ℂ ×
ℂ)) |
25 | 18, 23, 24 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ ×
ℂ)) |
26 | | fnssres 5918 |
. . . . . . . . 9
⊢ (( + Fn
(ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ)) →
( + ↾ (ran 𝐹 ×
ran 𝐺)) Fn (ran 𝐹 × ran 𝐺)) |
27 | 12, 25, 26 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) Fn (ran 𝐹 × ran 𝐺)) |
28 | | itg1add.4 |
. . . . . . . . 9
⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) |
29 | 28 | fneq1i 5899 |
. . . . . . . 8
⊢ (𝑃 Fn (ran 𝐹 × ran 𝐺) ↔ ( + ↾ (ran 𝐹 × ran 𝐺)) Fn (ran 𝐹 × ran 𝐺)) |
30 | 27, 29 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → 𝑃 Fn (ran 𝐹 × ran 𝐺)) |
31 | | dffn4 6034 |
. . . . . . 7
⊢ (𝑃 Fn (ran 𝐹 × ran 𝐺) ↔ 𝑃:(ran 𝐹 × ran 𝐺)–onto→ran 𝑃) |
32 | 30, 31 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝑃:(ran 𝐹 × ran 𝐺)–onto→ran 𝑃) |
33 | | fofi 8135 |
. . . . . 6
⊢ (((ran
𝐹 × ran 𝐺) ∈ Fin ∧ 𝑃:(ran 𝐹 × ran 𝐺)–onto→ran 𝑃) → ran 𝑃 ∈ Fin) |
34 | 9, 32, 33 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ran 𝑃 ∈ Fin) |
35 | | difss 3699 |
. . . . 5
⊢ (ran
𝑃 ∖ {0}) ⊆ ran
𝑃 |
36 | | ssfi 8065 |
. . . . 5
⊢ ((ran
𝑃 ∈ Fin ∧ (ran
𝑃 ∖ {0}) ⊆ ran
𝑃) → (ran 𝑃 ∖ {0}) ∈
Fin) |
37 | 34, 35, 36 | sylancl 693 |
. . . 4
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin) |
38 | | opelxpi 5072 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → 〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺)) |
39 | | ffun 5961 |
. . . . . . . . . . . 12
⊢ ( +
:(ℂ × ℂ)⟶ℂ → Fun + ) |
40 | 10, 39 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun
+ |
41 | 10 | fdmi 5965 |
. . . . . . . . . . . 12
⊢ dom + =
(ℂ × ℂ) |
42 | 25, 41 | syl6sseqr 3615 |
. . . . . . . . . . 11
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + ) |
43 | | funfvima2 6397 |
. . . . . . . . . . 11
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
44 | 40, 42, 43 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
45 | 38, 44 | syl5 33 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
46 | 45 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺))) |
47 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑥 + 𝑦) = ( + ‘〈𝑥, 𝑦〉) |
48 | 28 | rneqi 5273 |
. . . . . . . . 9
⊢ ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺)) |
49 | | df-ima 5051 |
. . . . . . . . 9
⊢ ( +
“ (ran 𝐹 × ran
𝐺)) = ran ( + ↾ (ran
𝐹 × ran 𝐺)) |
50 | 48, 49 | eqtr4i 2635 |
. . . . . . . 8
⊢ ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺)) |
51 | 46, 47, 50 | 3eltr4g 2705 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃) |
52 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
53 | 14, 52 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn ℝ) |
54 | | dffn3 5967 |
. . . . . . . 8
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
55 | 53, 54 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
56 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐺:ℝ⟶ℝ →
𝐺 Fn
ℝ) |
57 | 20, 56 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Fn ℝ) |
58 | | dffn3 5967 |
. . . . . . . 8
⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺) |
59 | 57, 58 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺) |
60 | | reex 9906 |
. . . . . . . 8
⊢ ℝ
∈ V |
61 | 60 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
V) |
62 | | inidm 3784 |
. . . . . . 7
⊢ (ℝ
∩ ℝ) = ℝ |
63 | 51, 55, 59, 61, 61, 62 | off 6810 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):ℝ⟶ran 𝑃) |
64 | | frn 5966 |
. . . . . 6
⊢ ((𝐹 ∘𝑓 +
𝐺):ℝ⟶ran 𝑃 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ran 𝑃) |
65 | 63, 64 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ran 𝑃) |
66 | 65 | ssdifd 3708 |
. . . 4
⊢ (𝜑 → (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0}) ⊆ (ran
𝑃 ∖
{0})) |
67 | 16 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ) |
68 | 22 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
69 | 67, 68 | anim12dan 878 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) |
70 | | readdcl 9898 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ) |
71 | 69, 70 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ) |
72 | 71 | ralrimivva 2954 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ) |
73 | | funimassov 6709 |
. . . . . . . 8
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(( + “ (ran 𝐹 ×
ran 𝐺)) ⊆ ℝ
↔ ∀𝑦 ∈ ran
𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)) |
74 | 40, 42, 73 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)) |
75 | 72, 74 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ) |
76 | 50, 75 | syl5eqss 3612 |
. . . . 5
⊢ (𝜑 → ran 𝑃 ⊆ ℝ) |
77 | 76 | ssdifd 3708 |
. . . 4
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖
{0})) |
78 | | itg1val2 23257 |
. . . 4
⊢ (((𝐹 ∘𝑓 +
𝐺) ∈ dom
∫1 ∧ ((ran 𝑃 ∖ {0}) ∈ Fin ∧ (ran (𝐹 ∘𝑓 +
𝐺) ∖ {0}) ⊆
(ran 𝑃 ∖ {0}) ∧
(ran 𝑃 ∖ {0}) ⊆
(ℝ ∖ {0}))) → (∫1‘(𝐹 ∘𝑓 + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤})))) |
79 | 3, 37, 66, 77, 78 | syl13anc 1320 |
. . 3
⊢ (𝜑 →
(∫1‘(𝐹
∘𝑓 + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤})))) |
80 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ) |
81 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin) |
82 | | inss2 3796 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) |
83 | 82 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})) |
84 | | i1fima 23251 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol) |
85 | 1, 84 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol) |
86 | | i1fima 23251 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) |
87 | 2, 86 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) |
88 | | inmbl 23117 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
89 | 85, 87, 88 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
90 | 89 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
91 | 35, 76 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆
ℝ) |
92 | 91 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ) |
93 | 92 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ) |
94 | 68 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
95 | 93, 94 | resubcld 10337 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 − 𝑧) ∈ ℝ) |
96 | 93 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ) |
97 | 94 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ) |
98 | 96, 97 | npcand 10275 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) = 𝑤) |
99 | | eldifsni 4261 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0) |
100 | 99 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0) |
101 | 98, 100 | eqnetrd 2849 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) ≠ 0) |
102 | | oveq12 6558 |
. . . . . . . . . . . . 13
⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = (0 + 0)) |
103 | | 00id 10090 |
. . . . . . . . . . . . 13
⊢ (0 + 0) =
0 |
104 | 102, 103 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = 0) |
105 | 104 | necon3ai 2807 |
. . . . . . . . . . 11
⊢ (((𝑤 − 𝑧) + 𝑧) ≠ 0 → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) |
106 | 101, 105 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) |
107 | | itg1add.3 |
. . . . . . . . . . 11
⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) |
108 | 1, 2, 107 | itg1addlem3 23271 |
. . . . . . . . . 10
⊢ ((((𝑤 − 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
109 | 95, 94, 106, 108 | syl21anc 1317 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
110 | 1, 2, 107 | itg1addlem2 23270 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
111 | 110 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
112 | 111, 95, 94 | fovrnd 6704 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ) |
113 | 109, 112 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
114 | 80, 81, 83, 90, 113 | itg1addlem1 23265 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
115 | 92 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ) |
116 | 1, 2 | i1faddlem 23266 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
117 | 115, 116 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
118 | 117 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤})) = (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
119 | 109 | sumeq2dv 14281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
120 | 114, 118,
119 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) |
121 | 120 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧))) |
122 | 112 | recnd 9947 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ) |
123 | 81, 115, 122 | fsummulc2 14358 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
124 | 121, 123 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
125 | 124 | sumeq2dv 14281 |
. . 3
⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
126 | 96, 122 | mulcld 9939 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
127 | 126 | anasss 677 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
128 | 37, 7, 127 | fsumcom 14349 |
. . 3
⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
129 | 79, 125, 128 | 3eqtrd 2648 |
. 2
⊢ (𝜑 →
(∫1‘(𝐹
∘𝑓 + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
130 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦 + 𝑧) = ((𝑤 − 𝑧) + 𝑧)) |
131 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦𝐼𝑧) = ((𝑤 − 𝑧)𝐼𝑧)) |
132 | 130, 131 | oveq12d 6567 |
. . . . . 6
⊢ (𝑦 = (𝑤 − 𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧))) |
133 | 34 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin) |
134 | 76 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ) |
135 | 134 | sselda 3568 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ) |
136 | 68 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ) |
137 | 135, 136 | resubcld 10337 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣 − 𝑧) ∈ ℝ) |
138 | 137 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣 − 𝑧) ∈ ℝ)) |
139 | 135 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ) |
140 | 139 | adantrr 749 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ) |
141 | 76 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ) |
142 | 141 | ad2ant2rl 781 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ) |
143 | 142 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ) |
144 | 68 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ) |
145 | 144 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ) |
146 | 140, 143,
145 | subcan2ad 10316 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦)) |
147 | 146 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦))) |
148 | 138, 147 | dom2lem 7881 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ) |
149 | | f1f1orn 6061 |
. . . . . . 7
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
150 | 148, 149 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
151 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑣 = 𝑤 → (𝑣 − 𝑧) = (𝑤 − 𝑧)) |
152 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) |
153 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑤 − 𝑧) ∈ V |
154 | 151, 152,
153 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧)) |
155 | 154 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧)) |
156 | | f1f 6014 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ) |
157 | | frn 5966 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ) |
158 | 148, 156,
157 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ) |
159 | 158 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑦 ∈ ℝ) |
160 | 68 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑧 ∈ ℝ) |
161 | 159, 160 | readdcld 9948 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦 + 𝑧) ∈ ℝ) |
162 | 110 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
163 | 162, 159,
160 | fovrnd 6704 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦𝐼𝑧) ∈ ℝ) |
164 | 161, 163 | remulcld 9949 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ) |
165 | 164 | recnd 9947 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
166 | 132, 133,
150, 155, 165 | fsumf1o 14301 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧))) |
167 | 134 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ) |
168 | 167 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ) |
169 | 144 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ) |
170 | 168, 169 | npcand 10275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤 − 𝑧) + 𝑧) = 𝑤) |
171 | 170 | oveq1d 6564 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = (𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
172 | 171 | sumeq2dv 14281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
173 | 166, 172 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
174 | 42 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + ) |
175 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
176 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺) |
177 | | opelxpi 5072 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺) → 〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺)) |
178 | 175, 176,
177 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺)) |
179 | | funfvima2 6397 |
. . . . . . . . . . . 12
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
180 | 40, 179 | mpan 702 |
. . . . . . . . . . 11
⊢ ((ran
𝐹 × ran 𝐺) ⊆ dom + →
(〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
181 | 174, 178,
180 | sylc 63 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺))) |
182 | | df-ov 6552 |
. . . . . . . . . 10
⊢ (𝑦 + 𝑧) = ( + ‘〈𝑦, 𝑧〉) |
183 | 181, 182,
50 | 3eltr4g 2705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃) |
184 | 67 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ) |
185 | 184 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ) |
186 | 144 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ) |
187 | 185, 186 | pncand 10272 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦) |
188 | 187 | eqcomd 2616 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧)) |
189 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑦 + 𝑧) → (𝑣 − 𝑧) = ((𝑦 + 𝑧) − 𝑧)) |
190 | 189 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑦 + 𝑧) → (𝑦 = (𝑣 − 𝑧) ↔ 𝑦 = ((𝑦 + 𝑧) − 𝑧))) |
191 | 190 | rspcev 3282 |
. . . . . . . . 9
⊢ (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
192 | 183, 188,
191 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
193 | 192 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
194 | | ssabral 3636 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} ↔ ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
195 | 193, 194 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)}) |
196 | 152 | rnmpt 5292 |
. . . . . 6
⊢ ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} |
197 | 195, 196 | syl6sseqr 3615 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
198 | 68 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ) |
199 | 184, 198 | readdcld 9948 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ) |
200 | 110 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
201 | 200, 184,
198 | fovrnd 6704 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ) |
202 | 199, 201 | remulcld 9949 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ) |
203 | 202 | recnd 9947 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
204 | 158 | ssdifd 3708 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹)) |
205 | 204 | sselda 3568 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹)) |
206 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (ℝ ∖ ran
𝐹) → 𝑦 ∈
ℝ) |
207 | 206 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ) |
208 | 68 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ) |
209 | | simprr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0)) |
210 | 1, 2, 107 | itg1addlem3 23271 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬
(𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})))) |
211 | 207, 208,
209, 210 | syl21anc 1317 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})))) |
212 | | inss1 3795 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {𝑦}) |
213 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (ℝ ∖ ran
𝐹) → ¬ 𝑦 ∈ ran 𝐹) |
214 | 213 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹) |
215 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
216 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑣 ∈ V |
217 | 216 | eliniseg 5413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ V → (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)) |
218 | 215, 217 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦) |
219 | 216, 215 | brelrn 5277 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣𝐹𝑦 → 𝑦 ∈ ran 𝐹) |
220 | 218, 219 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ (◡𝐹 “ {𝑦}) → 𝑦 ∈ ran 𝐹) |
221 | 214, 220 | nsyl 134 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑣 ∈ (◡𝐹 “ {𝑦})) |
222 | 221 | pm2.21d 117 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑣 ∈ (◡𝐹 “ {𝑦}) → 𝑣 ∈ ∅)) |
223 | 222 | ssrdv 3574 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (◡𝐹 “ {𝑦}) ⊆ ∅) |
224 | 212, 223 | syl5ss 3579 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅) |
225 | | ss0 3926 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅ → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅) |
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅) |
227 | 226 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = (vol‘∅)) |
228 | | 0mbl 23114 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ dom vol |
229 | | mblvol 23105 |
. . . . . . . . . . . . . 14
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
230 | 228, 229 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(vol‘∅) = (vol*‘∅) |
231 | | ovol0 23068 |
. . . . . . . . . . . . 13
⊢
(vol*‘∅) = 0 |
232 | 230, 231 | eqtri 2632 |
. . . . . . . . . . . 12
⊢
(vol‘∅) = 0 |
233 | 227, 232 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = 0) |
234 | 211, 233 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0) |
235 | 234 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0)) |
236 | 207, 208 | readdcld 9948 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ) |
237 | 236 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ) |
238 | 237 | mul01d 10114 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0) |
239 | 235, 238 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
240 | 239 | expr 641 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)) |
241 | | oveq12 6558 |
. . . . . . . . . 10
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0)) |
242 | 241, 103 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0) |
243 | | oveq12 6558 |
. . . . . . . . . 10
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0)) |
244 | | 0re 9919 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
245 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) = 0) |
246 | | c0ex 9913 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
247 | 245, 107,
246 | ovmpt2a 6689 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0) |
248 | 244, 244,
247 | mp2an 704 |
. . . . . . . . . 10
⊢ (0𝐼0) = 0 |
249 | 243, 248 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0) |
250 | 242, 249 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0)) |
251 | | 0cn 9911 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
252 | 251 | mul01i 10105 |
. . . . . . . 8
⊢ (0
· 0) = 0 |
253 | 250, 252 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
254 | 240, 253 | pm2.61d2 171 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
255 | 205, 254 | syldan 486 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
256 | | f1ofo 6057 |
. . . . . . 7
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
257 | 150, 256 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
258 | | fofi 8135 |
. . . . . 6
⊢ ((ran
𝑃 ∈ Fin ∧ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin) |
259 | 133, 257,
258 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin) |
260 | 197, 203,
255, 259 | fsumss 14303 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |
261 | 35 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) |
262 | 126 | an32s 842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
263 | | dfin4 3826 |
. . . . . . . 8
⊢ (ran
𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) |
264 | | inss2 3796 |
. . . . . . . 8
⊢ (ran
𝑃 ∩ {0}) ⊆
{0} |
265 | 263, 264 | eqsstr3i 3599 |
. . . . . . 7
⊢ (ran
𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆
{0} |
266 | 265 | sseli 3564 |
. . . . . 6
⊢ (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0}) |
267 | | elsni 4142 |
. . . . . . . . 9
⊢ (𝑤 ∈ {0} → 𝑤 = 0) |
268 | 267 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0) |
269 | 268 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = (0 · ((𝑤 − 𝑧)𝐼𝑧))) |
270 | 110 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
271 | 268, 244 | syl6eqel 2696 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ) |
272 | 68 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ) |
273 | 271, 272 | resubcld 10337 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 − 𝑧) ∈ ℝ) |
274 | 270, 273,
272 | fovrnd 6704 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ) |
275 | 274 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ) |
276 | 275 | mul02d 10113 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
277 | 269, 276 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
278 | 266, 277 | sylan2 490 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
279 | 261, 262,
278, 133 | fsumss 14303 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
280 | 173, 260,
279 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
281 | 280 | sumeq2dv 14281 |
. 2
⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
282 | 203 | anasss 677 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
283 | 7, 5, 282 | fsumcom 14349 |
. 2
⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |
284 | 129, 281,
283 | 3eqtr2d 2650 |
1
⊢ (𝜑 →
(∫1‘(𝐹
∘𝑓 + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |