Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
2 | | i1fadd.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
3 | 1, 2 | i1fadd 23899 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ dom
∫1) |
4 | | i1frn 23881 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
6 | | i1frn 23881 |
. . . . . . . 8
⊢ (𝐺 ∈ dom ∫1
→ ran 𝐺 ∈
Fin) |
7 | 2, 6 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
8 | | xpfi 8519 |
. . . . . . 7
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) |
9 | 5, 7, 8 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) |
10 | | ax-addf 10351 |
. . . . . . . . . 10
⊢ +
:(ℂ × ℂ)⟶ℂ |
11 | | ffn 6291 |
. . . . . . . . . 10
⊢ ( +
:(ℂ × ℂ)⟶ℂ → + Fn (ℂ ×
ℂ)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢ + Fn
(ℂ × ℂ) |
13 | | i1ff 23880 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
14 | 1, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
15 | 14 | frnd 6298 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
16 | | ax-resscn 10329 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
17 | 15, 16 | syl6ss 3832 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
18 | | i1ff 23880 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
19 | 2, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
20 | 19 | frnd 6298 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐺 ⊆ ℝ) |
21 | 20, 16 | syl6ss 3832 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝐺 ⊆ ℂ) |
22 | | xpss12 5370 |
. . . . . . . . . 10
⊢ ((ran
𝐹 ⊆ ℂ ∧ ran
𝐺 ⊆ ℂ) →
(ran 𝐹 × ran 𝐺) ⊆ (ℂ ×
ℂ)) |
23 | 17, 21, 22 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ ×
ℂ)) |
24 | | fnssres 6250 |
. . . . . . . . 9
⊢ (( + Fn
(ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ)) →
( + ↾ (ran 𝐹 ×
ran 𝐺)) Fn (ran 𝐹 × ran 𝐺)) |
25 | 12, 23, 24 | sylancr 581 |
. . . . . . . 8
⊢ (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) Fn (ran 𝐹 × ran 𝐺)) |
26 | | itg1add.4 |
. . . . . . . . 9
⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) |
27 | 26 | fneq1i 6230 |
. . . . . . . 8
⊢ (𝑃 Fn (ran 𝐹 × ran 𝐺) ↔ ( + ↾ (ran 𝐹 × ran 𝐺)) Fn (ran 𝐹 × ran 𝐺)) |
28 | 25, 27 | sylibr 226 |
. . . . . . 7
⊢ (𝜑 → 𝑃 Fn (ran 𝐹 × ran 𝐺)) |
29 | | dffn4 6372 |
. . . . . . 7
⊢ (𝑃 Fn (ran 𝐹 × ran 𝐺) ↔ 𝑃:(ran 𝐹 × ran 𝐺)–onto→ran 𝑃) |
30 | 28, 29 | sylib 210 |
. . . . . 6
⊢ (𝜑 → 𝑃:(ran 𝐹 × ran 𝐺)–onto→ran 𝑃) |
31 | | fofi 8540 |
. . . . . 6
⊢ (((ran
𝐹 × ran 𝐺) ∈ Fin ∧ 𝑃:(ran 𝐹 × ran 𝐺)–onto→ran 𝑃) → ran 𝑃 ∈ Fin) |
32 | 9, 30, 31 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → ran 𝑃 ∈ Fin) |
33 | | difss 3959 |
. . . . 5
⊢ (ran
𝑃 ∖ {0}) ⊆ ran
𝑃 |
34 | | ssfi 8468 |
. . . . 5
⊢ ((ran
𝑃 ∈ Fin ∧ (ran
𝑃 ∖ {0}) ⊆ ran
𝑃) → (ran 𝑃 ∖ {0}) ∈
Fin) |
35 | 32, 33, 34 | sylancl 580 |
. . . 4
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin) |
36 | | opelxpi 5392 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → 〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺)) |
37 | | ffun 6294 |
. . . . . . . . . . . 12
⊢ ( +
:(ℂ × ℂ)⟶ℂ → Fun + ) |
38 | 10, 37 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun
+ |
39 | 10 | fdmi 6301 |
. . . . . . . . . . . 12
⊢ dom + =
(ℂ × ℂ) |
40 | 23, 39 | syl6sseqr 3870 |
. . . . . . . . . . 11
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + ) |
41 | | funfvima2 6765 |
. . . . . . . . . . 11
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
42 | 38, 40, 41 | sylancr 581 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
43 | 36, 42 | syl5 34 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
44 | 43 | imp 397 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺))) |
45 | | df-ov 6925 |
. . . . . . . 8
⊢ (𝑥 + 𝑦) = ( + ‘〈𝑥, 𝑦〉) |
46 | 26 | rneqi 5597 |
. . . . . . . . 9
⊢ ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺)) |
47 | | df-ima 5368 |
. . . . . . . . 9
⊢ ( +
“ (ran 𝐹 × ran
𝐺)) = ran ( + ↾ (ran
𝐹 × ran 𝐺)) |
48 | 46, 47 | eqtr4i 2804 |
. . . . . . . 8
⊢ ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺)) |
49 | 44, 45, 48 | 3eltr4g 2875 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃) |
50 | 14 | ffnd 6292 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn ℝ) |
51 | | dffn3 6302 |
. . . . . . . 8
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
52 | 50, 51 | sylib 210 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
53 | 19 | ffnd 6292 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Fn ℝ) |
54 | | dffn3 6302 |
. . . . . . . 8
⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺) |
55 | 53, 54 | sylib 210 |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺) |
56 | | reex 10363 |
. . . . . . . 8
⊢ ℝ
∈ V |
57 | 56 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
V) |
58 | | inidm 4042 |
. . . . . . 7
⊢ (ℝ
∩ ℝ) = ℝ |
59 | 49, 52, 55, 57, 57, 58 | off 7189 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):ℝ⟶ran 𝑃) |
60 | 59 | frnd 6298 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ran 𝑃) |
61 | 60 | ssdifd 3968 |
. . . 4
⊢ (𝜑 → (ran (𝐹 ∘𝑓 + 𝐺) ∖ {0}) ⊆ (ran
𝑃 ∖
{0})) |
62 | 15 | sselda 3820 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ) |
63 | 20 | sselda 3820 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
64 | 62, 63 | anim12dan 612 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) |
65 | | readdcl 10355 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ) |
66 | 64, 65 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ) |
67 | 66 | ralrimivva 3152 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ) |
68 | | funimassov 7088 |
. . . . . . . 8
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(( + “ (ran 𝐹 ×
ran 𝐺)) ⊆ ℝ
↔ ∀𝑦 ∈ ran
𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)) |
69 | 38, 40, 68 | sylancr 581 |
. . . . . . 7
⊢ (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)) |
70 | 67, 69 | mpbird 249 |
. . . . . 6
⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ) |
71 | 48, 70 | syl5eqss 3867 |
. . . . 5
⊢ (𝜑 → ran 𝑃 ⊆ ℝ) |
72 | 71 | ssdifd 3968 |
. . . 4
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖
{0})) |
73 | | itg1val2 23888 |
. . . 4
⊢ (((𝐹 ∘𝑓 +
𝐺) ∈ dom
∫1 ∧ ((ran 𝑃 ∖ {0}) ∈ Fin ∧ (ran (𝐹 ∘𝑓 +
𝐺) ∖ {0}) ⊆
(ran 𝑃 ∖ {0}) ∧
(ran 𝑃 ∖ {0}) ⊆
(ℝ ∖ {0}))) → (∫1‘(𝐹 ∘𝑓 + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤})))) |
74 | 3, 35, 61, 72, 73 | syl13anc 1440 |
. . 3
⊢ (𝜑 →
(∫1‘(𝐹
∘𝑓 + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤})))) |
75 | 19 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ) |
76 | 7 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin) |
77 | | inss2 4053 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) |
78 | 77 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})) |
79 | | i1fima 23882 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol) |
80 | 1, 79 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol) |
81 | | i1fima 23882 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) |
82 | 2, 81 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) |
83 | | inmbl 23746 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
84 | 80, 82, 83 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
85 | 84 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
86 | 33, 71 | syl5ss 3831 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆
ℝ) |
87 | 86 | sselda 3820 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ) |
88 | 87 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ) |
89 | 63 | adantlr 705 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
90 | 88, 89 | resubcld 10803 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 − 𝑧) ∈ ℝ) |
91 | 88 | recnd 10405 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ) |
92 | 89 | recnd 10405 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ) |
93 | 91, 92 | npcand 10738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) = 𝑤) |
94 | | eldifsni 4553 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0) |
95 | 94 | ad2antlr 717 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0) |
96 | 93, 95 | eqnetrd 3035 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) ≠ 0) |
97 | | oveq12 6931 |
. . . . . . . . . . . . 13
⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = (0 + 0)) |
98 | | 00id 10551 |
. . . . . . . . . . . . 13
⊢ (0 + 0) =
0 |
99 | 97, 98 | syl6eq 2829 |
. . . . . . . . . . . 12
⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = 0) |
100 | 99 | necon3ai 2993 |
. . . . . . . . . . 11
⊢ (((𝑤 − 𝑧) + 𝑧) ≠ 0 → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) |
101 | 96, 100 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) |
102 | | itg1add.3 |
. . . . . . . . . . 11
⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) |
103 | 1, 2, 102 | itg1addlem3 23902 |
. . . . . . . . . 10
⊢ ((((𝑤 − 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
104 | 90, 89, 101, 103 | syl21anc 828 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
105 | 1, 2, 102 | itg1addlem2 23901 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
106 | 105 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
107 | 106, 90, 89 | fovrnd 7083 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ) |
108 | 104, 107 | eqeltrrd 2859 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
109 | 75, 76, 78, 85, 108 | itg1addlem1 23896 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
110 | 87 | recnd 10405 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ) |
111 | 1, 2 | i1faddlem 23897 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
112 | 110, 111 | syldan 585 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
113 | 112 | fveq2d 6450 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤})) = (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
114 | 104 | sumeq2dv 14841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
115 | 109, 113,
114 | 3eqtr4d 2823 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) |
116 | 115 | oveq2d 6938 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧))) |
117 | 107 | recnd 10405 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ) |
118 | 76, 110, 117 | fsummulc2 14920 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
119 | 116, 118 | eqtrd 2813 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
120 | 119 | sumeq2dv 14841 |
. . 3
⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
121 | 91, 117 | mulcld 10397 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
122 | 121 | anasss 460 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
123 | 35, 7, 122 | fsumcom 14911 |
. . 3
⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
124 | 74, 120, 123 | 3eqtrd 2817 |
. 2
⊢ (𝜑 →
(∫1‘(𝐹
∘𝑓 + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
125 | | oveq1 6929 |
. . . . . . 7
⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦 + 𝑧) = ((𝑤 − 𝑧) + 𝑧)) |
126 | | oveq1 6929 |
. . . . . . 7
⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦𝐼𝑧) = ((𝑤 − 𝑧)𝐼𝑧)) |
127 | 125, 126 | oveq12d 6940 |
. . . . . 6
⊢ (𝑦 = (𝑤 − 𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧))) |
128 | 32 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin) |
129 | 71 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ) |
130 | 129 | sselda 3820 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ) |
131 | 63 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ) |
132 | 130, 131 | resubcld 10803 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣 − 𝑧) ∈ ℝ) |
133 | 132 | ex 403 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣 − 𝑧) ∈ ℝ)) |
134 | 130 | recnd 10405 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ) |
135 | 134 | adantrr 707 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ) |
136 | 71 | sselda 3820 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ) |
137 | 136 | ad2ant2rl 739 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ) |
138 | 137 | recnd 10405 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ) |
139 | 63 | recnd 10405 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ) |
140 | 139 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ) |
141 | 135, 138,
140 | subcan2ad 10779 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦)) |
142 | 141 | ex 403 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦))) |
143 | 133, 142 | dom2lem 8281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ) |
144 | | f1f1orn 6402 |
. . . . . . 7
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
145 | 143, 144 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
146 | | oveq1 6929 |
. . . . . . . 8
⊢ (𝑣 = 𝑤 → (𝑣 − 𝑧) = (𝑤 − 𝑧)) |
147 | | eqid 2777 |
. . . . . . . 8
⊢ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) |
148 | | ovex 6954 |
. . . . . . . 8
⊢ (𝑤 − 𝑧) ∈ V |
149 | 146, 147,
148 | fvmpt 6542 |
. . . . . . 7
⊢ (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧)) |
150 | 149 | adantl 475 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧)) |
151 | | f1f 6351 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ) |
152 | | frn 6297 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ) |
153 | 143, 151,
152 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ) |
154 | 153 | sselda 3820 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑦 ∈ ℝ) |
155 | 63 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑧 ∈ ℝ) |
156 | 154, 155 | readdcld 10406 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦 + 𝑧) ∈ ℝ) |
157 | 105 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
158 | 157, 154,
155 | fovrnd 7083 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦𝐼𝑧) ∈ ℝ) |
159 | 156, 158 | remulcld 10407 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ) |
160 | 159 | recnd 10405 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
161 | 127, 128,
145, 150, 160 | fsumf1o 14861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧))) |
162 | 129 | sselda 3820 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ) |
163 | 162 | recnd 10405 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ) |
164 | 139 | adantr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ) |
165 | 163, 164 | npcand 10738 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤 − 𝑧) + 𝑧) = 𝑤) |
166 | 165 | oveq1d 6937 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = (𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
167 | 166 | sumeq2dv 14841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
168 | 161, 167 | eqtrd 2813 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
169 | 40 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + ) |
170 | | simpr 479 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
171 | | simplr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺) |
172 | | opelxpi 5392 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺) → 〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺)) |
173 | 170, 171,
172 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺)) |
174 | | funfvima2 6765 |
. . . . . . . . . . . 12
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
175 | 38, 174 | mpan 680 |
. . . . . . . . . . 11
⊢ ((ran
𝐹 × ran 𝐺) ⊆ dom + →
(〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
176 | 169, 173,
175 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺))) |
177 | | df-ov 6925 |
. . . . . . . . . 10
⊢ (𝑦 + 𝑧) = ( + ‘〈𝑦, 𝑧〉) |
178 | 176, 177,
48 | 3eltr4g 2875 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃) |
179 | 62 | adantlr 705 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ) |
180 | 179 | recnd 10405 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ) |
181 | 139 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ) |
182 | 180, 181 | pncand 10735 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦) |
183 | 182 | eqcomd 2783 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧)) |
184 | | oveq1 6929 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑦 + 𝑧) → (𝑣 − 𝑧) = ((𝑦 + 𝑧) − 𝑧)) |
185 | 184 | rspceeqv 3528 |
. . . . . . . . 9
⊢ (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
186 | 178, 183,
185 | syl2anc 579 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
187 | 186 | ralrimiva 3147 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
188 | | ssabral 3893 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} ↔ ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
189 | 187, 188 | sylibr 226 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)}) |
190 | 147 | rnmpt 5617 |
. . . . . 6
⊢ ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} |
191 | 189, 190 | syl6sseqr 3870 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
192 | 63 | adantr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ) |
193 | 179, 192 | readdcld 10406 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ) |
194 | 105 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
195 | 194, 179,
192 | fovrnd 7083 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ) |
196 | 193, 195 | remulcld 10407 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ) |
197 | 196 | recnd 10405 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
198 | 153 | ssdifd 3968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹)) |
199 | 198 | sselda 3820 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹)) |
200 | | eldifi 3954 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (ℝ ∖ ran
𝐹) → 𝑦 ∈
ℝ) |
201 | 200 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ) |
202 | 63 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ) |
203 | | simprr 763 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0)) |
204 | 1, 2, 102 | itg1addlem3 23902 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬
(𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})))) |
205 | 201, 202,
203, 204 | syl21anc 828 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})))) |
206 | | inss1 4052 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {𝑦}) |
207 | | eldifn 3955 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (ℝ ∖ ran
𝐹) → ¬ 𝑦 ∈ ran 𝐹) |
208 | 207 | ad2antrl 718 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹) |
209 | | vex 3400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
210 | | vex 3400 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑣 ∈ V |
211 | 210 | eliniseg 5748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ V → (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)) |
212 | 209, 211 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦) |
213 | 210, 209 | brelrn 5602 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣𝐹𝑦 → 𝑦 ∈ ran 𝐹) |
214 | 212, 213 | sylbi 209 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ (◡𝐹 “ {𝑦}) → 𝑦 ∈ ran 𝐹) |
215 | 208, 214 | nsyl 138 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑣 ∈ (◡𝐹 “ {𝑦})) |
216 | 215 | pm2.21d 119 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑣 ∈ (◡𝐹 “ {𝑦}) → 𝑣 ∈ ∅)) |
217 | 216 | ssrdv 3826 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (◡𝐹 “ {𝑦}) ⊆ ∅) |
218 | 206, 217 | syl5ss 3831 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅) |
219 | | ss0 4199 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅ → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅) |
220 | 218, 219 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅) |
221 | 220 | fveq2d 6450 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = (vol‘∅)) |
222 | | 0mbl 23743 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ dom vol |
223 | | mblvol 23734 |
. . . . . . . . . . . . . 14
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
224 | 222, 223 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(vol‘∅) = (vol*‘∅) |
225 | | ovol0 23697 |
. . . . . . . . . . . . 13
⊢
(vol*‘∅) = 0 |
226 | 224, 225 | eqtri 2801 |
. . . . . . . . . . . 12
⊢
(vol‘∅) = 0 |
227 | 221, 226 | syl6eq 2829 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = 0) |
228 | 205, 227 | eqtrd 2813 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0) |
229 | 228 | oveq2d 6938 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0)) |
230 | 201, 202 | readdcld 10406 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ) |
231 | 230 | recnd 10405 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ) |
232 | 231 | mul01d 10575 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0) |
233 | 229, 232 | eqtrd 2813 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
234 | 233 | expr 450 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)) |
235 | | oveq12 6931 |
. . . . . . . . . 10
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0)) |
236 | 235, 98 | syl6eq 2829 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0) |
237 | | oveq12 6931 |
. . . . . . . . . 10
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0)) |
238 | | 0re 10378 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
239 | | iftrue 4312 |
. . . . . . . . . . . 12
⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) = 0) |
240 | | c0ex 10370 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
241 | 239, 102,
240 | ovmpt2a 7068 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0) |
242 | 238, 238,
241 | mp2an 682 |
. . . . . . . . . 10
⊢ (0𝐼0) = 0 |
243 | 237, 242 | syl6eq 2829 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0) |
244 | 236, 243 | oveq12d 6940 |
. . . . . . . 8
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0)) |
245 | | 0cn 10368 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
246 | 245 | mul01i 10566 |
. . . . . . . 8
⊢ (0
· 0) = 0 |
247 | 244, 246 | syl6eq 2829 |
. . . . . . 7
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
248 | 234, 247 | pm2.61d2 174 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
249 | 199, 248 | syldan 585 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
250 | | f1ofo 6398 |
. . . . . . 7
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
251 | 145, 250 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
252 | | fofi 8540 |
. . . . . 6
⊢ ((ran
𝑃 ∈ Fin ∧ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin) |
253 | 128, 251,
252 | syl2anc 579 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin) |
254 | 191, 197,
249, 253 | fsumss 14863 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |
255 | 33 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) |
256 | 121 | an32s 642 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
257 | | dfin4 4093 |
. . . . . . . 8
⊢ (ran
𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) |
258 | | inss2 4053 |
. . . . . . . 8
⊢ (ran
𝑃 ∩ {0}) ⊆
{0} |
259 | 257, 258 | eqsstr3i 3854 |
. . . . . . 7
⊢ (ran
𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆
{0} |
260 | 259 | sseli 3816 |
. . . . . 6
⊢ (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0}) |
261 | | elsni 4414 |
. . . . . . . . 9
⊢ (𝑤 ∈ {0} → 𝑤 = 0) |
262 | 261 | adantl 475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0) |
263 | 262 | oveq1d 6937 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = (0 · ((𝑤 − 𝑧)𝐼𝑧))) |
264 | 105 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
265 | 262, 238 | syl6eqel 2866 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ) |
266 | 63 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ) |
267 | 265, 266 | resubcld 10803 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 − 𝑧) ∈ ℝ) |
268 | 264, 267,
266 | fovrnd 7083 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ) |
269 | 268 | recnd 10405 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ) |
270 | 269 | mul02d 10574 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
271 | 263, 270 | eqtrd 2813 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
272 | 260, 271 | sylan2 586 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
273 | 255, 256,
272, 128 | fsumss 14863 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
274 | 168, 254,
273 | 3eqtr4d 2823 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
275 | 274 | sumeq2dv 14841 |
. 2
⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
276 | 197 | anasss 460 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
277 | 7, 5, 276 | fsumcom 14911 |
. 2
⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |
278 | 124, 275,
277 | 3eqtr2d 2819 |
1
⊢ (𝜑 →
(∫1‘(𝐹
∘𝑓 + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |