Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
2 | | i1fadd.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
3 | 1, 2 | i1fadd 24857 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ dom
∫1) |
4 | | itg1add.4 |
. . . . . . 7
⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺)) |
5 | | ax-addf 10951 |
. . . . . . . . 9
⊢ +
:(ℂ × ℂ)⟶ℂ |
6 | | ffn 6598 |
. . . . . . . . 9
⊢ ( +
:(ℂ × ℂ)⟶ℂ → + Fn (ℂ ×
ℂ)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
⊢ + Fn
(ℂ × ℂ) |
8 | | i1frn 24839 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
10 | | i1frn 24839 |
. . . . . . . . . 10
⊢ (𝐺 ∈ dom ∫1
→ ran 𝐺 ∈
Fin) |
11 | 2, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
12 | | xpfi 9063 |
. . . . . . . . 9
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) |
13 | 9, 11, 12 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) |
14 | | resfnfinfin 9077 |
. . . . . . . 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 9080 |
. . . . . 6
⊢ (𝑃 ∈ Fin → ran 𝑃 ∈ Fin) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → ran 𝑃 ∈ Fin) |
19 | | difss 4071 |
. . . . 5
⊢ (ran
𝑃 ∖ {0}) ⊆ ran
𝑃 |
20 | | ssfi 8938 |
. . . . 5
⊢ ((ran
𝑃 ∈ Fin ∧ (ran
𝑃 ∖ {0}) ⊆ ran
𝑃) → (ran 𝑃 ∖ {0}) ∈
Fin) |
21 | 18, 19, 20 | sylancl 586 |
. . . 4
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin) |
22 | | ffun 6601 |
. . . . . . . . . . 11
⊢ ( +
:(ℂ × ℂ)⟶ℂ → Fun + ) |
23 | 5, 22 | ax-mp 5 |
. . . . . . . . . 10
⊢ Fun
+ |
24 | | i1ff 24838 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
25 | 1, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
26 | 25 | frnd 6606 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
27 | | ax-resscn 10929 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
28 | 26, 27 | sstrdi 3938 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
29 | | i1ff 24838 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ dom ∫1
→ 𝐺:ℝ⟶ℝ) |
30 | 2, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:ℝ⟶ℝ) |
31 | 30 | frnd 6606 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐺 ⊆ ℝ) |
32 | 31, 27 | sstrdi 3938 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐺 ⊆ ℂ) |
33 | | xpss12 5605 |
. . . . . . . . . . . 12
⊢ ((ran
𝐹 ⊆ ℂ ∧ ran
𝐺 ⊆ ℂ) →
(ran 𝐹 × ran 𝐺) ⊆ (ℂ ×
ℂ)) |
34 | 28, 32, 33 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ ×
ℂ)) |
35 | 5 | fdmi 6610 |
. . . . . . . . . . 11
⊢ dom + =
(ℂ × ℂ) |
36 | 34, 35 | sseqtrrdi 3977 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + ) |
37 | | funfvima2 7104 |
. . . . . . . . . 10
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
38 | 23, 36, 37 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
39 | | opelxpi 5627 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → 〈𝑥, 𝑦〉 ∈ (ran 𝐹 × ran 𝐺)) |
40 | 38, 39 | impel 506 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → ( + ‘〈𝑥, 𝑦〉) ∈ ( + “ (ran 𝐹 × ran 𝐺))) |
41 | | df-ov 7274 |
. . . . . . . 8
⊢ (𝑥 + 𝑦) = ( + ‘〈𝑥, 𝑦〉) |
42 | 4 | rneqi 5845 |
. . . . . . . . 9
⊢ ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺)) |
43 | | df-ima 5603 |
. . . . . . . . 9
⊢ ( +
“ (ran 𝐹 × ran
𝐺)) = ran ( + ↾ (ran
𝐹 × ran 𝐺)) |
44 | 42, 43 | eqtr4i 2771 |
. . . . . . . 8
⊢ ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺)) |
45 | 40, 41, 44 | 3eltr4g 2858 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃) |
46 | 25 | ffnd 6599 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn ℝ) |
47 | | dffn3 6611 |
. . . . . . . 8
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
48 | 46, 47 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
49 | 30 | ffnd 6599 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Fn ℝ) |
50 | | dffn3 6611 |
. . . . . . . 8
⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺) |
51 | 49, 50 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺) |
52 | | reex 10963 |
. . . . . . . 8
⊢ ℝ
∈ V |
53 | 52 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
V) |
54 | | inidm 4158 |
. . . . . . 7
⊢ (ℝ
∩ ℝ) = ℝ |
55 | 45, 48, 51, 53, 53, 54 | off 7545 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘f + 𝐺):ℝ⟶ran 𝑃) |
56 | 55 | frnd 6606 |
. . . . 5
⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ran 𝑃) |
57 | 56 | ssdifd 4080 |
. . . 4
⊢ (𝜑 → (ran (𝐹 ∘f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0})) |
58 | 26 | sselda 3926 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ) |
59 | 31 | sselda 3926 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
60 | 58, 59 | anim12dan 619 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) |
61 | | readdcl 10955 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ) |
62 | 60, 61 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ) |
63 | 62 | ralrimivva 3117 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ) |
64 | | funimassov 7443 |
. . . . . . . 8
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(( + “ (ran 𝐹 ×
ran 𝐺)) ⊆ ℝ
↔ ∀𝑦 ∈ ran
𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)) |
65 | 23, 36, 64 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)) |
66 | 63, 65 | mpbird 256 |
. . . . . 6
⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ) |
67 | 44, 66 | eqsstrid 3974 |
. . . . 5
⊢ (𝜑 → ran 𝑃 ⊆ ℝ) |
68 | 67 | ssdifd 4080 |
. . . 4
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖
{0})) |
69 | | itg1val2 24846 |
. . . 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 1371 |
. . 3
⊢ (𝜑 →
(∫1‘(𝐹
∘f + 𝐺)) =
Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤})))) |
71 | 30 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ) |
72 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin) |
73 | | inss2 4169 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}) |
74 | 73 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})) |
75 | | i1fima 24840 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol) |
76 | 1, 75 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol) |
77 | | i1fima 24840 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑧}) ∈ dom vol) |
78 | 2, 77 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol) |
79 | | inmbl 24704 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol ∧ (◡𝐺 “ {𝑧}) ∈ dom vol) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
80 | 76, 78, 79 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
81 | 80 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ∈ dom vol) |
82 | 19, 67 | sstrid 3937 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆
ℝ) |
83 | 82 | sselda 3926 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ) |
84 | 83 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ) |
85 | 59 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ) |
86 | 84, 85 | resubcld 11403 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 − 𝑧) ∈ ℝ) |
87 | 84 | recnd 11004 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ) |
88 | 85 | recnd 11004 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ) |
89 | 87, 88 | npcand 11336 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) = 𝑤) |
90 | | eldifsni 4729 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0) |
91 | 90 | ad2antlr 724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0) |
92 | 89, 91 | eqnetrd 3013 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) ≠ 0) |
93 | | oveq12 7280 |
. . . . . . . . . . . . 13
⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = (0 + 0)) |
94 | | 00id 11150 |
. . . . . . . . . . . . 13
⊢ (0 + 0) =
0 |
95 | 93, 94 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = 0) |
96 | 95 | necon3ai 2970 |
. . . . . . . . . . 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 24860 |
. . . . . . . . . 10
⊢ ((((𝑤 − 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
100 | 86, 85, 97, 99 | syl21anc 835 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
101 | 1, 2, 98 | itg1addlem2 24859 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
102 | 101 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
103 | 102, 86, 85 | fovrnd 7438 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ) |
104 | 100, 103 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ) |
105 | 71, 72, 74, 81, 104 | itg1addlem1 24854 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
106 | 83 | recnd 11004 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ) |
107 | 1, 2 | i1faddlem 24855 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (◡(𝐹 ∘f + 𝐺) “ {𝑤}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
108 | 106, 107 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (◡(𝐹 ∘f + 𝐺) “ {𝑤}) = ∪
𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) |
109 | 108 | fveq2d 6775 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤})) = (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
110 | 100 | sumeq2dv 15413 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))) |
111 | 105, 109,
110 | 3eqtr4d 2790 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) |
112 | 111 | oveq2d 7287 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧))) |
113 | 103 | recnd 11004 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ) |
114 | 72, 106, 113 | fsummulc2 15494 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
115 | 112, 114 | eqtrd 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
116 | 115 | sumeq2dv 15413 |
. . 3
⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
117 | 87, 113 | mulcld 10996 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
118 | 117 | anasss 467 |
. . . 4
⊢ ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
119 | 21, 11, 118 | fsumcom 15485 |
. . 3
⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
120 | 70, 116, 119 | 3eqtrd 2784 |
. 2
⊢ (𝜑 →
(∫1‘(𝐹
∘f + 𝐺)) =
Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
121 | | oveq1 7278 |
. . . . . . 7
⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦 + 𝑧) = ((𝑤 − 𝑧) + 𝑧)) |
122 | | oveq1 7278 |
. . . . . . 7
⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦𝐼𝑧) = ((𝑤 − 𝑧)𝐼𝑧)) |
123 | 121, 122 | oveq12d 7289 |
. . . . . 6
⊢ (𝑦 = (𝑤 − 𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧))) |
124 | 18 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin) |
125 | 67 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ) |
126 | 125 | sselda 3926 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ) |
127 | 59 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ) |
128 | 126, 127 | resubcld 11403 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣 − 𝑧) ∈ ℝ) |
129 | 128 | ex 413 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣 − 𝑧) ∈ ℝ)) |
130 | 126 | recnd 11004 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ) |
131 | 130 | adantrr 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ) |
132 | 67 | sselda 3926 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ) |
133 | 132 | ad2ant2rl 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ) |
134 | 133 | recnd 11004 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ) |
135 | 59 | recnd 11004 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ) |
136 | 135 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ) |
137 | 131, 134,
136 | subcan2ad 11377 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦)) |
138 | 137 | ex 413 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦))) |
139 | 129, 138 | dom2lem 8763 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ) |
140 | | f1f1orn 6725 |
. . . . . . 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 7278 |
. . . . . . . 8
⊢ (𝑣 = 𝑤 → (𝑣 − 𝑧) = (𝑤 − 𝑧)) |
143 | | eqid 2740 |
. . . . . . . 8
⊢ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) |
144 | | ovex 7304 |
. . . . . . . 8
⊢ (𝑤 − 𝑧) ∈ V |
145 | 142, 143,
144 | fvmpt 6872 |
. . . . . . 7
⊢ (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧)) |
146 | 145 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧)) |
147 | | f1f 6668 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ) |
148 | | frn 6605 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ) |
149 | 139, 147,
148 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ) |
150 | 149 | sselda 3926 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑦 ∈ ℝ) |
151 | 59 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑧 ∈ ℝ) |
152 | 150, 151 | readdcld 11005 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦 + 𝑧) ∈ ℝ) |
153 | 101 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
154 | 153, 150,
151 | fovrnd 7438 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦𝐼𝑧) ∈ ℝ) |
155 | 152, 154 | remulcld 11006 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ) |
156 | 155 | recnd 11004 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
157 | 123, 124,
141, 146, 156 | fsumf1o 15433 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧))) |
158 | 125 | sselda 3926 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ) |
159 | 158 | recnd 11004 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ) |
160 | 135 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ) |
161 | 159, 160 | npcand 11336 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤 − 𝑧) + 𝑧) = 𝑤) |
162 | 161 | oveq1d 7286 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = (𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
163 | 162 | sumeq2dv 15413 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
164 | 157, 163 | eqtrd 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
165 | 36 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + ) |
166 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
167 | | simplr 766 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺) |
168 | 166, 167 | opelxpd 5628 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺)) |
169 | | funfvima2 7104 |
. . . . . . . . . . . 12
⊢ ((Fun +
∧ (ran 𝐹 × ran
𝐺) ⊆ dom + ) →
(〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
170 | 23, 169 | mpan 687 |
. . . . . . . . . . 11
⊢ ((ran
𝐹 × ran 𝐺) ⊆ dom + →
(〈𝑦, 𝑧〉 ∈ (ran 𝐹 × ran 𝐺) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺)))) |
171 | 165, 168,
170 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘〈𝑦, 𝑧〉) ∈ ( + “ (ran 𝐹 × ran 𝐺))) |
172 | | df-ov 7274 |
. . . . . . . . . 10
⊢ (𝑦 + 𝑧) = ( + ‘〈𝑦, 𝑧〉) |
173 | 171, 172,
44 | 3eltr4g 2858 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃) |
174 | 58 | adantlr 712 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ) |
175 | 174 | recnd 11004 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ) |
176 | 135 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ) |
177 | 175, 176 | pncand 11333 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦) |
178 | 177 | eqcomd 2746 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧)) |
179 | | oveq1 7278 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑦 + 𝑧) → (𝑣 − 𝑧) = ((𝑦 + 𝑧) − 𝑧)) |
180 | 179 | rspceeqv 3576 |
. . . . . . . . 9
⊢ (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
181 | 173, 178,
180 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
182 | 181 | ralrimiva 3110 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
183 | | ssabral 4001 |
. . . . . . 7
⊢ (ran
𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} ↔ ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)) |
184 | 182, 183 | sylibr 233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)}) |
185 | 143 | rnmpt 5863 |
. . . . . 6
⊢ ran
(𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} |
186 | 184, 185 | sseqtrrdi 3977 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) |
187 | 59 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ) |
188 | 174, 187 | readdcld 11005 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ) |
189 | 101 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
190 | 189, 174,
187 | fovrnd 7438 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ) |
191 | 188, 190 | remulcld 11006 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ) |
192 | 191 | recnd 11004 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
193 | 149 | ssdifd 4080 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹)) |
194 | 193 | sselda 3926 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹)) |
195 | | eldifi 4066 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (ℝ ∖ ran
𝐹) → 𝑦 ∈
ℝ) |
196 | 195 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ) |
197 | 59 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ) |
198 | | simprr 770 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0)) |
199 | 1, 2, 98 | itg1addlem3 24860 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬
(𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})))) |
200 | 196, 197,
198, 199 | syl21anc 835 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})))) |
201 | | inss1 4168 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {𝑦}) |
202 | | eldifn 4067 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (ℝ ∖ ran
𝐹) → ¬ 𝑦 ∈ ran 𝐹) |
203 | 202 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹) |
204 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑣 ∈ V |
205 | 204 | eliniseg 6001 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ V → (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)) |
206 | 205 | elv 3437 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦) |
207 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑦 ∈ V |
208 | 204, 207 | brelrn 5850 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣𝐹𝑦 → 𝑦 ∈ ran 𝐹) |
209 | 206, 208 | sylbi 216 |
. . . . . . . . . . . . . . . . . 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 3932 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (◡𝐹 “ {𝑦}) ⊆ ∅) |
213 | 201, 212 | sstrid 3937 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅) |
214 | | ss0 4338 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅ → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅) |
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅) |
216 | 215 | fveq2d 6775 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = (vol‘∅)) |
217 | | 0mbl 24701 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ dom vol |
218 | | mblvol 24692 |
. . . . . . . . . . . . . 14
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
219 | 217, 218 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(vol‘∅) = (vol*‘∅) |
220 | | ovol0 24655 |
. . . . . . . . . . . . 13
⊢
(vol*‘∅) = 0 |
221 | 219, 220 | eqtri 2768 |
. . . . . . . . . . . 12
⊢
(vol‘∅) = 0 |
222 | 216, 221 | eqtrdi 2796 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = 0) |
223 | 200, 222 | eqtrd 2780 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0) |
224 | 223 | oveq2d 7287 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0)) |
225 | 196, 197 | readdcld 11005 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ) |
226 | 225 | recnd 11004 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ) |
227 | 226 | mul01d 11174 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0) |
228 | 224, 227 | eqtrd 2780 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0) |
229 | 228 | expr 457 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)) |
230 | | oveq12 7280 |
. . . . . . . . . 10
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0)) |
231 | 230, 94 | eqtrdi 2796 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0) |
232 | | oveq12 7280 |
. . . . . . . . . 10
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0)) |
233 | | 0re 10978 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
234 | | iftrue 4471 |
. . . . . . . . . . . 12
⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) = 0) |
235 | | c0ex 10970 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
236 | 234, 98, 235 | ovmpoa 7422 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0) |
237 | 233, 233,
236 | mp2an 689 |
. . . . . . . . . 10
⊢ (0𝐼0) = 0 |
238 | 232, 237 | eqtrdi 2796 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0) |
239 | 231, 238 | oveq12d 7289 |
. . . . . . . 8
⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0)) |
240 | | 0cn 10968 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
241 | 240 | mul01i 11165 |
. . . . . . . 8
⊢ (0
· 0) = 0 |
242 | 239, 241 | eqtrdi 2796 |
. . . . . . 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 6721 |
. . . . . . 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 9083 |
. . . . . 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 15435 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |
250 | 19 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) |
251 | 117 | an32s 649 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ) |
252 | | dfin4 4207 |
. . . . . . . 8
⊢ (ran
𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) |
253 | | inss2 4169 |
. . . . . . . 8
⊢ (ran
𝑃 ∩ {0}) ⊆
{0} |
254 | 252, 253 | eqsstrri 3961 |
. . . . . . 7
⊢ (ran
𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆
{0} |
255 | 254 | sseli 3922 |
. . . . . 6
⊢ (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0}) |
256 | | elsni 4584 |
. . . . . . . . 9
⊢ (𝑤 ∈ {0} → 𝑤 = 0) |
257 | 256 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0) |
258 | 257 | oveq1d 7286 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = (0 · ((𝑤 − 𝑧)𝐼𝑧))) |
259 | 101 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ ×
ℝ)⟶ℝ) |
260 | 257, 233 | eqeltrdi 2849 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ) |
261 | 59 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ) |
262 | 260, 261 | resubcld 11403 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 − 𝑧) ∈ ℝ) |
263 | 259, 262,
261 | fovrnd 7438 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ) |
264 | 263 | recnd 11004 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ) |
265 | 264 | mul02d 11173 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
266 | 258, 265 | eqtrd 2780 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
267 | 255, 266 | sylan2 593 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0) |
268 | 250, 251,
267, 124 | fsumss 15435 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
269 | 164, 249,
268 | 3eqtr4d 2790 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
270 | 269 | sumeq2dv 15413 |
. 2
⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧))) |
271 | 192 | anasss 467 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ) |
272 | 11, 9, 271 | fsumcom 15485 |
. 2
⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |
273 | 120, 270,
272 | 3eqtr2d 2786 |
1
⊢ (𝜑 →
(∫1‘(𝐹
∘f + 𝐺)) =
Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧))) |