MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg1addlem4 Structured version   Visualization version   GIF version

Theorem itg1addlem4 25747
Description: Lemma for itg1add 25750. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof shortened by SN, 3-Oct-2024.)
Hypotheses
Ref Expression
i1fadd.1 (𝜑𝐹 ∈ dom ∫1)
i1fadd.2 (𝜑𝐺 ∈ dom ∫1)
itg1add.3 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((𝐹 “ {𝑖}) ∩ (𝐺 “ {𝑗})))))
itg1add.4 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))
Assertion
Ref Expression
itg1addlem4 (𝜑 → (∫1‘(𝐹f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
Distinct variable groups:   𝑖,𝑗,𝑦,𝑧   𝑦,𝐼   𝑦,𝑃,𝑧   𝑖,𝐹,𝑗,𝑦,𝑧   𝑖,𝐺,𝑗,𝑦,𝑧   𝜑,𝑖,𝑗,𝑦,𝑧
Allowed substitution hints:   𝑃(𝑖,𝑗)   𝐼(𝑧,𝑖,𝑗)

Proof of Theorem itg1addlem4
Dummy variables 𝑤 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 i1fadd.1 . . . . 5 (𝜑𝐹 ∈ dom ∫1)
2 i1fadd.2 . . . . 5 (𝜑𝐺 ∈ dom ∫1)
31, 2i1fadd 25743 . . . 4 (𝜑 → (𝐹f + 𝐺) ∈ dom ∫1)
4 itg1add.4 . . . . . . 7 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))
5 ax-addf 11231 . . . . . . . . 9 + :(ℂ × ℂ)⟶ℂ
6 ffn 6736 . . . . . . . . 9 ( + :(ℂ × ℂ)⟶ℂ → + Fn (ℂ × ℂ))
75, 6ax-mp 5 . . . . . . . 8 + Fn (ℂ × ℂ)
8 i1frn 25725 . . . . . . . . . 10 (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)
91, 8syl 17 . . . . . . . . 9 (𝜑 → ran 𝐹 ∈ Fin)
10 i1frn 25725 . . . . . . . . . 10 (𝐺 ∈ dom ∫1 → ran 𝐺 ∈ Fin)
112, 10syl 17 . . . . . . . . 9 (𝜑 → ran 𝐺 ∈ Fin)
12 xpfi 9355 . . . . . . . . 9 ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) → (ran 𝐹 × ran 𝐺) ∈ Fin)
139, 11, 12syl2anc 584 . . . . . . . 8 (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin)
14 resfnfinfin 9374 . . . . . . . 8 (( + Fn (ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ∈ Fin) → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
157, 13, 14sylancr 587 . . . . . . 7 (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
164, 15eqeltrid 2842 . . . . . 6 (𝜑𝑃 ∈ Fin)
17 rnfi 9377 . . . . . 6 (𝑃 ∈ Fin → ran 𝑃 ∈ Fin)
1816, 17syl 17 . . . . 5 (𝜑 → ran 𝑃 ∈ Fin)
19 difss 4145 . . . . 5 (ran 𝑃 ∖ {0}) ⊆ ran 𝑃
20 ssfi 9211 . . . . 5 ((ran 𝑃 ∈ Fin ∧ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) → (ran 𝑃 ∖ {0}) ∈ Fin)
2118, 19, 20sylancl 586 . . . 4 (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin)
22 ffun 6739 . . . . . . . . . . 11 ( + :(ℂ × ℂ)⟶ℂ → Fun + )
235, 22ax-mp 5 . . . . . . . . . 10 Fun +
24 i1ff 25724 . . . . . . . . . . . . . . 15 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
251, 24syl 17 . . . . . . . . . . . . . 14 (𝜑𝐹:ℝ⟶ℝ)
2625frnd 6744 . . . . . . . . . . . . 13 (𝜑 → ran 𝐹 ⊆ ℝ)
27 ax-resscn 11209 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
2826, 27sstrdi 4007 . . . . . . . . . . . 12 (𝜑 → ran 𝐹 ⊆ ℂ)
29 i1ff 25724 . . . . . . . . . . . . . . 15 (𝐺 ∈ dom ∫1𝐺:ℝ⟶ℝ)
302, 29syl 17 . . . . . . . . . . . . . 14 (𝜑𝐺:ℝ⟶ℝ)
3130frnd 6744 . . . . . . . . . . . . 13 (𝜑 → ran 𝐺 ⊆ ℝ)
3231, 27sstrdi 4007 . . . . . . . . . . . 12 (𝜑 → ran 𝐺 ⊆ ℂ)
33 xpss12 5703 . . . . . . . . . . . 12 ((ran 𝐹 ⊆ ℂ ∧ ran 𝐺 ⊆ ℂ) → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
3428, 32, 33syl2anc 584 . . . . . . . . . . 11 (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
355fdmi 6747 . . . . . . . . . . 11 dom + = (ℂ × ℂ)
3634, 35sseqtrrdi 4046 . . . . . . . . . 10 (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + )
37 funfvima2 7250 . . . . . . . . . 10 ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
3823, 36, 37sylancr 587 . . . . . . . . 9 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
39 opelxpi 5725 . . . . . . . . 9 ((𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺) → ⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺))
4038, 39impel 505 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺)) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
41 df-ov 7433 . . . . . . . 8 (𝑥 + 𝑦) = ( + ‘⟨𝑥, 𝑦⟩)
424rneqi 5950 . . . . . . . . 9 ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺))
43 df-ima 5701 . . . . . . . . 9 ( + “ (ran 𝐹 × ran 𝐺)) = ran ( + ↾ (ran 𝐹 × ran 𝐺))
4442, 43eqtr4i 2765 . . . . . . . 8 ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺))
4540, 41, 443eltr4g 2855 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃)
4625ffnd 6737 . . . . . . . 8 (𝜑𝐹 Fn ℝ)
47 dffn3 6748 . . . . . . . 8 (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹)
4846, 47sylib 218 . . . . . . 7 (𝜑𝐹:ℝ⟶ran 𝐹)
4930ffnd 6737 . . . . . . . 8 (𝜑𝐺 Fn ℝ)
50 dffn3 6748 . . . . . . . 8 (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺)
5149, 50sylib 218 . . . . . . 7 (𝜑𝐺:ℝ⟶ran 𝐺)
52 reex 11243 . . . . . . . 8 ℝ ∈ V
5352a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ V)
54 inidm 4234 . . . . . . 7 (ℝ ∩ ℝ) = ℝ
5545, 48, 51, 53, 53, 54off 7714 . . . . . 6 (𝜑 → (𝐹f + 𝐺):ℝ⟶ran 𝑃)
5655frnd 6744 . . . . 5 (𝜑 → ran (𝐹f + 𝐺) ⊆ ran 𝑃)
5756ssdifd 4154 . . . 4 (𝜑 → (ran (𝐹f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}))
5826sselda 3994 . . . . . . . . . 10 ((𝜑𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
5931sselda 3994 . . . . . . . . . 10 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
6058, 59anim12dan 619 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
61 readdcl 11235 . . . . . . . . 9 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ)
6260, 61syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ)
6362ralrimivva 3199 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)
64 funimassov 7609 . . . . . . . 8 ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
6523, 36, 64sylancr 587 . . . . . . 7 (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
6663, 65mpbird 257 . . . . . 6 (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ)
6744, 66eqsstrid 4043 . . . . 5 (𝜑 → ran 𝑃 ⊆ ℝ)
6867ssdifd 4154 . . . 4 (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖ {0}))
69 itg1val2 25732 . . . 4 (((𝐹f + 𝐺) ∈ dom ∫1 ∧ ((ran 𝑃 ∖ {0}) ∈ Fin ∧ (ran (𝐹f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}) ∧ (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖ {0}))) → (∫1‘(𝐹f + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘((𝐹f + 𝐺) “ {𝑤}))))
703, 21, 57, 68, 69syl13anc 1371 . . 3 (𝜑 → (∫1‘(𝐹f + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘((𝐹f + 𝐺) “ {𝑤}))))
7130adantr 480 . . . . . . . 8 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ)
7211adantr 480 . . . . . . . 8 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin)
73 inss2 4245 . . . . . . . . 9 ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐺 “ {𝑧})
7473a1i 11 . . . . . . . 8 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐺 “ {𝑧}))
75 i1fima 25726 . . . . . . . . . . 11 (𝐹 ∈ dom ∫1 → (𝐹 “ {(𝑤𝑧)}) ∈ dom vol)
761, 75syl 17 . . . . . . . . . 10 (𝜑 → (𝐹 “ {(𝑤𝑧)}) ∈ dom vol)
77 i1fima 25726 . . . . . . . . . . 11 (𝐺 ∈ dom ∫1 → (𝐺 “ {𝑧}) ∈ dom vol)
782, 77syl 17 . . . . . . . . . 10 (𝜑 → (𝐺 “ {𝑧}) ∈ dom vol)
79 inmbl 25590 . . . . . . . . . 10 (((𝐹 “ {(𝑤𝑧)}) ∈ dom vol ∧ (𝐺 “ {𝑧}) ∈ dom vol) → ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
8076, 78, 79syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
8180ad2antrr 726 . . . . . . . 8 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
8219, 67sstrid 4006 . . . . . . . . . . . . 13 (𝜑 → (ran 𝑃 ∖ {0}) ⊆ ℝ)
8382sselda 3994 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ)
8483adantr 480 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ)
8559adantlr 715 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
8684, 85resubcld 11688 . . . . . . . . . 10 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤𝑧) ∈ ℝ)
8784recnd 11286 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ)
8885recnd 11286 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
8987, 88npcand 11621 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧) + 𝑧) = 𝑤)
90 eldifsni 4794 . . . . . . . . . . . . 13 (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0)
9190ad2antlr 727 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0)
9289, 91eqnetrd 3005 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧) + 𝑧) ≠ 0)
93 oveq12 7439 . . . . . . . . . . . . 13 (((𝑤𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤𝑧) + 𝑧) = (0 + 0))
94 00id 11433 . . . . . . . . . . . . 13 (0 + 0) = 0
9593, 94eqtrdi 2790 . . . . . . . . . . . 12 (((𝑤𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤𝑧) + 𝑧) = 0)
9695necon3ai 2962 . . . . . . . . . . 11 (((𝑤𝑧) + 𝑧) ≠ 0 → ¬ ((𝑤𝑧) = 0 ∧ 𝑧 = 0))
9792, 96syl 17 . . . . . . . . . 10 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ¬ ((𝑤𝑧) = 0 ∧ 𝑧 = 0))
98 itg1add.3 . . . . . . . . . . 11 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((𝐹 “ {𝑖}) ∩ (𝐺 “ {𝑗})))))
991, 2, 98itg1addlem3 25746 . . . . . . . . . 10 ((((𝑤𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤𝑧)𝐼𝑧) = (vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
10086, 85, 97, 99syl21anc 838 . . . . . . . . 9 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧)𝐼𝑧) = (vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
1011, 2, 98itg1addlem2 25745 . . . . . . . . . . 11 (𝜑𝐼:(ℝ × ℝ)⟶ℝ)
102101ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ × ℝ)⟶ℝ)
103102, 86, 85fovcdmd 7604 . . . . . . . . 9 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧)𝐼𝑧) ∈ ℝ)
104100, 103eqeltrrd 2839 . . . . . . . 8 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)
10571, 72, 74, 81, 104itg1addlem1 25740 . . . . . . 7 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘ 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
10683recnd 11286 . . . . . . . . 9 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ)
1071, 2i1faddlem 25741 . . . . . . . . 9 ((𝜑𝑤 ∈ ℂ) → ((𝐹f + 𝐺) “ {𝑤}) = 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})))
108106, 107syldan 591 . . . . . . . 8 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → ((𝐹f + 𝐺) “ {𝑤}) = 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})))
109108fveq2d 6910 . . . . . . 7 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘((𝐹f + 𝐺) “ {𝑤})) = (vol‘ 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
110100sumeq2dv 15734 . . . . . . 7 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
111105, 109, 1103eqtr4d 2784 . . . . . 6 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘((𝐹f + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤𝑧)𝐼𝑧))
112111oveq2d 7446 . . . . 5 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘((𝐹f + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤𝑧)𝐼𝑧)))
113103recnd 11286 . . . . . 6 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧)𝐼𝑧) ∈ ℂ)
11472, 106, 113fsummulc2 15816 . . . . 5 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤𝑧)𝐼𝑧)))
115112, 114eqtrd 2774 . . . 4 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘((𝐹f + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤𝑧)𝐼𝑧)))
116115sumeq2dv 15734 . . 3 (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘((𝐹f + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤𝑧)𝐼𝑧)))
11787, 113mulcld 11278 . . . . 5 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) ∈ ℂ)
118117anasss 466 . . . 4 ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) ∈ ℂ)
11921, 11, 118fsumcom 15807 . . 3 (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)))
12070, 116, 1193eqtrd 2778 . 2 (𝜑 → (∫1‘(𝐹f + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)))
121 oveq1 7437 . . . . . . 7 (𝑦 = (𝑤𝑧) → (𝑦 + 𝑧) = ((𝑤𝑧) + 𝑧))
122 oveq1 7437 . . . . . . 7 (𝑦 = (𝑤𝑧) → (𝑦𝐼𝑧) = ((𝑤𝑧)𝐼𝑧))
123121, 122oveq12d 7448 . . . . . 6 (𝑦 = (𝑤𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤𝑧) + 𝑧) · ((𝑤𝑧)𝐼𝑧)))
12418adantr 480 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin)
12567adantr 480 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ)
126125sselda 3994 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ)
12759adantr 480 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ)
128126, 127resubcld 11688 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣𝑧) ∈ ℝ)
129128ex 412 . . . . . . . 8 ((𝜑𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣𝑧) ∈ ℝ))
130126recnd 11286 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ)
131130adantrr 717 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ)
13267sselda 3994 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ)
133132ad2ant2rl 749 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ)
134133recnd 11286 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ)
13559recnd 11286 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
136135adantr 480 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ)
137131, 134, 136subcan2ad 11662 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → ((𝑣𝑧) = (𝑦𝑧) ↔ 𝑣 = 𝑦))
138137ex 412 . . . . . . . 8 ((𝜑𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃) → ((𝑣𝑧) = (𝑦𝑧) ↔ 𝑣 = 𝑦)))
139129, 138dom2lem 9030 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃1-1→ℝ)
140 f1f1orn 6859 . . . . . . 7 ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃1-1-onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)))
141139, 140syl 17 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃1-1-onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)))
142 oveq1 7437 . . . . . . . 8 (𝑣 = 𝑤 → (𝑣𝑧) = (𝑤𝑧))
143 eqid 2734 . . . . . . . 8 (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))
144 ovex 7463 . . . . . . . 8 (𝑤𝑧) ∈ V
145142, 143, 144fvmpt 7015 . . . . . . 7 (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))‘𝑤) = (𝑤𝑧))
146145adantl 481 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))‘𝑤) = (𝑤𝑧))
147 f1f 6804 . . . . . . . . . . 11 ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃⟶ℝ)
148 frn 6743 . . . . . . . . . . 11 ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ⊆ ℝ)
149139, 147, 1483syl 18 . . . . . . . . . 10 ((𝜑𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ⊆ ℝ)
150149sselda 3994 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → 𝑦 ∈ ℝ)
15159adantr 480 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → 𝑧 ∈ ℝ)
152150, 151readdcld 11287 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → (𝑦 + 𝑧) ∈ ℝ)
153101ad2antrr 726 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → 𝐼:(ℝ × ℝ)⟶ℝ)
154153, 150, 151fovcdmd 7604 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → (𝑦𝐼𝑧) ∈ ℝ)
155152, 154remulcld 11288 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
156155recnd 11286 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
157123, 124, 141, 146, 156fsumf1o 15755 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤𝑧) + 𝑧) · ((𝑤𝑧)𝐼𝑧)))
158125sselda 3994 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ)
159158recnd 11286 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ)
160135adantr 480 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ)
161159, 160npcand 11621 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤𝑧) + 𝑧) = 𝑤)
162161oveq1d 7445 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤𝑧) + 𝑧) · ((𝑤𝑧)𝐼𝑧)) = (𝑤 · ((𝑤𝑧)𝐼𝑧)))
163162sumeq2dv 15734 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤𝑧) + 𝑧) · ((𝑤𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤𝑧)𝐼𝑧)))
164157, 163eqtrd 2774 . . . 4 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤𝑧)𝐼𝑧)))
16536ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + )
166 simpr 484 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹)
167 simplr 769 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺)
168166, 167opelxpd 5727 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺))
169 funfvima2 7250 . . . . . . . . . . . 12 ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
17023, 169mpan 690 . . . . . . . . . . 11 ((ran 𝐹 × ran 𝐺) ⊆ dom + → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
171165, 168, 170sylc 65 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
172 df-ov 7433 . . . . . . . . . 10 (𝑦 + 𝑧) = ( + ‘⟨𝑦, 𝑧⟩)
173171, 172, 443eltr4g 2855 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃)
17458adantlr 715 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
175174recnd 11286 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ)
176135adantr 480 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ)
177175, 176pncand 11618 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦)
178177eqcomd 2740 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧))
179 oveq1 7437 . . . . . . . . . 10 (𝑣 = (𝑦 + 𝑧) → (𝑣𝑧) = ((𝑦 + 𝑧) − 𝑧))
180179rspceeqv 3644 . . . . . . . . 9 (((𝑦 + 𝑧) ∈ ran 𝑃𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧))
181173, 178, 180syl2anc 584 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧))
182181ralrimiva 3143 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧))
183 ssabral 4074 . . . . . . 7 (ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧)} ↔ ∀𝑦 ∈ ran 𝐹𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧))
184182, 183sylibr 234 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧)})
185143rnmpt 5970 . . . . . 6 ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧)}
186184, 185sseqtrrdi 4046 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)))
18759adantr 480 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ)
188174, 187readdcld 11287 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ)
189101ad2antrr 726 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ × ℝ)⟶ℝ)
190189, 174, 187fovcdmd 7604 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ)
191188, 190remulcld 11288 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
192191recnd 11286 . . . . 5 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
193149ssdifd 4154 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹))
194193sselda 3994 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹))
195 eldifi 4140 . . . . . . . . . . . . 13 (𝑦 ∈ (ℝ ∖ ran 𝐹) → 𝑦 ∈ ℝ)
196195ad2antrl 728 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ)
19759adantr 480 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ)
198 simprr 773 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0))
1991, 2, 98itg1addlem3 25746 . . . . . . . . . . . 12 (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧}))))
200196, 197, 198, 199syl21anc 838 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧}))))
201 inss1 4244 . . . . . . . . . . . . . . 15 ((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐹 “ {𝑦})
202 eldifn 4141 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (ℝ ∖ ran 𝐹) → ¬ 𝑦 ∈ ran 𝐹)
203202ad2antrl 728 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹)
204 vex 3481 . . . . . . . . . . . . . . . . . . . . 21 𝑣 ∈ V
205204eliniseg 6114 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ V → (𝑣 ∈ (𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦))
206205elv 3482 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ (𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)
207 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
208204, 207brelrn 5955 . . . . . . . . . . . . . . . . . . 19 (𝑣𝐹𝑦𝑦 ∈ ran 𝐹)
209206, 208sylbi 217 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ (𝐹 “ {𝑦}) → 𝑦 ∈ ran 𝐹)
210203, 209nsyl 140 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑣 ∈ (𝐹 “ {𝑦}))
211210pm2.21d 121 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑣 ∈ (𝐹 “ {𝑦}) → 𝑣 ∈ ∅))
212211ssrdv 4000 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝐹 “ {𝑦}) ⊆ ∅)
213201, 212sstrid 4006 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) ⊆ ∅)
214 ss0 4407 . . . . . . . . . . . . . 14 (((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) ⊆ ∅ → ((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) = ∅)
215213, 214syl 17 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) = ∅)
216215fveq2d 6910 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧}))) = (vol‘∅))
217 0mbl 25587 . . . . . . . . . . . . . 14 ∅ ∈ dom vol
218 mblvol 25578 . . . . . . . . . . . . . 14 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
219217, 218ax-mp 5 . . . . . . . . . . . . 13 (vol‘∅) = (vol*‘∅)
220 ovol0 25541 . . . . . . . . . . . . 13 (vol*‘∅) = 0
221219, 220eqtri 2762 . . . . . . . . . . . 12 (vol‘∅) = 0
222216, 221eqtrdi 2790 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧}))) = 0)
223200, 222eqtrd 2774 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0)
224223oveq2d 7446 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0))
225196, 197readdcld 11287 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ)
226225recnd 11286 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ)
227226mul01d 11457 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0)
228224, 227eqtrd 2774 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
229228expr 456 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0))
230 oveq12 7439 . . . . . . . . . 10 ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0))
231230, 94eqtrdi 2790 . . . . . . . . 9 ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0)
232 oveq12 7439 . . . . . . . . . 10 ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0))
233 0re 11260 . . . . . . . . . . 11 0 ∈ ℝ
234 iftrue 4536 . . . . . . . . . . . 12 ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((𝐹 “ {𝑖}) ∩ (𝐺 “ {𝑗})))) = 0)
235 c0ex 11252 . . . . . . . . . . . 12 0 ∈ V
236234, 98, 235ovmpoa 7587 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0)
237233, 233, 236mp2an 692 . . . . . . . . . 10 (0𝐼0) = 0
238232, 237eqtrdi 2790 . . . . . . . . 9 ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0)
239231, 238oveq12d 7448 . . . . . . . 8 ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0))
240 0cn 11250 . . . . . . . . 9 0 ∈ ℂ
241240mul01i 11448 . . . . . . . 8 (0 · 0) = 0
242239, 241eqtrdi 2790 . . . . . . 7 ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
243229, 242pm2.61d2 181 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
244194, 243syldan 591 . . . . 5 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
245 f1ofo 6855 . . . . . . 7 ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃1-1-onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) → (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)))
246141, 245syl 17 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)))
247 fofi 9348 . . . . . 6 ((ran 𝑃 ∈ Fin ∧ (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∈ Fin)
248124, 246, 247syl2anc 584 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∈ Fin)
249186, 192, 244, 248fsumss 15757 . . . 4 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
25019a1i 11 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃)
251117an32s 652 . . . . 5 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) ∈ ℂ)
252 dfin4 4283 . . . . . . . 8 (ran 𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))
253 inss2 4245 . . . . . . . 8 (ran 𝑃 ∩ {0}) ⊆ {0}
254252, 253eqsstrri 4030 . . . . . . 7 (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆ {0}
255254sseli 3990 . . . . . 6 (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0})
256 elsni 4647 . . . . . . . . 9 (𝑤 ∈ {0} → 𝑤 = 0)
257256adantl 481 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0)
258257oveq1d 7445 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) = (0 · ((𝑤𝑧)𝐼𝑧)))
259101ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ × ℝ)⟶ℝ)
260257, 233eqeltrdi 2846 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ)
26159adantr 480 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ)
262260, 261resubcld 11688 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤𝑧) ∈ ℝ)
263259, 262, 261fovcdmd 7604 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤𝑧)𝐼𝑧) ∈ ℝ)
264263recnd 11286 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤𝑧)𝐼𝑧) ∈ ℂ)
265264mul02d 11456 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤𝑧)𝐼𝑧)) = 0)
266258, 265eqtrd 2774 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) = 0)
267255, 266sylan2 593 . . . . 5 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) = 0)
268250, 251, 267, 124fsumss 15757 . . . 4 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤𝑧)𝐼𝑧)))
269164, 249, 2683eqtr4d 2784 . . 3 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)))
270269sumeq2dv 15734 . 2 (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)))
271192anasss 466 . . 3 ((𝜑 ∧ (𝑧 ∈ ran 𝐺𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
27211, 9, 271fsumcom 15807 . 2 (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
273120, 270, 2723eqtr2d 2780 1 (𝜑 → (∫1‘(𝐹f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  {cab 2711  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cdif 3959  cin 3961  wss 3962  c0 4338  ifcif 4530  {csn 4630  cop 4636   ciun 4995   class class class wbr 5147  cmpt 5230   × cxp 5686  ccnv 5687  dom cdm 5688  ran crn 5689  cres 5690  cima 5691  Fun wfun 6556   Fn wfn 6557  wf 6558  1-1wf1 6559  ontowfo 6560  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  cmpo 7432  f cof 7694  Fincfn 8983  cc 11150  cr 11151  0cc0 11152   + caddc 11155   · cmul 11157  cmin 11489  Σcsu 15718  vol*covol 25510  volcvol 25511  1citg1 25663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-oi 9547  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-q 12988  df-rp 13032  df-xadd 13152  df-ioo 13387  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-xmet 21374  df-met 21375  df-ovol 25512  df-vol 25513  df-mbf 25667  df-itg1 25668
This theorem is referenced by:  itg1addlem5  25749
  Copyright terms: Public domain W3C validator