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

Theorem itg1addlem4 24861
Description: Lemma for itg1add 24864. (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 24857 . . . 4 (𝜑 → (𝐹f + 𝐺) ∈ dom ∫1)
4 itg1add.4 . . . . . . 7 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))
5 ax-addf 10951 . . . . . . . . 9 + :(ℂ × ℂ)⟶ℂ
6 ffn 6598 . . . . . . . . 9 ( + :(ℂ × ℂ)⟶ℂ → + Fn (ℂ × ℂ))
75, 6ax-mp 5 . . . . . . . 8 + Fn (ℂ × ℂ)
8 i1frn 24839 . . . . . . . . . 10 (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)
91, 8syl 17 . . . . . . . . 9 (𝜑 → ran 𝐹 ∈ Fin)
10 i1frn 24839 . . . . . . . . . 10 (𝐺 ∈ dom ∫1 → ran 𝐺 ∈ Fin)
112, 10syl 17 . . . . . . . . 9 (𝜑 → ran 𝐺 ∈ Fin)
12 xpfi 9063 . . . . . . . . 9 ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) → (ran 𝐹 × ran 𝐺) ∈ Fin)
139, 11, 12syl2anc 584 . . . . . . . 8 (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin)
14 resfnfinfin 9077 . . . . . . . 8 (( + Fn (ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ∈ Fin) → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
157, 13, 14sylancr 587 . . . . . . 7 (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
164, 15eqeltrid 2845 . . . . . 6 (𝜑𝑃 ∈ Fin)
17 rnfi 9080 . . . . . 6 (𝑃 ∈ Fin → ran 𝑃 ∈ Fin)
1816, 17syl 17 . . . . 5 (𝜑 → ran 𝑃 ∈ Fin)
19 difss 4071 . . . . 5 (ran 𝑃 ∖ {0}) ⊆ ran 𝑃
20 ssfi 8938 . . . . 5 ((ran 𝑃 ∈ Fin ∧ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) → (ran 𝑃 ∖ {0}) ∈ Fin)
2118, 19, 20sylancl 586 . . . 4 (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin)
22 ffun 6601 . . . . . . . . . . 11 ( + :(ℂ × ℂ)⟶ℂ → Fun + )
235, 22ax-mp 5 . . . . . . . . . 10 Fun +
24 i1ff 24838 . . . . . . . . . . . . . . 15 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
251, 24syl 17 . . . . . . . . . . . . . 14 (𝜑𝐹:ℝ⟶ℝ)
2625frnd 6606 . . . . . . . . . . . . 13 (𝜑 → ran 𝐹 ⊆ ℝ)
27 ax-resscn 10929 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
2826, 27sstrdi 3938 . . . . . . . . . . . 12 (𝜑 → ran 𝐹 ⊆ ℂ)
29 i1ff 24838 . . . . . . . . . . . . . . 15 (𝐺 ∈ dom ∫1𝐺:ℝ⟶ℝ)
302, 29syl 17 . . . . . . . . . . . . . 14 (𝜑𝐺:ℝ⟶ℝ)
3130frnd 6606 . . . . . . . . . . . . 13 (𝜑 → ran 𝐺 ⊆ ℝ)
3231, 27sstrdi 3938 . . . . . . . . . . . 12 (𝜑 → ran 𝐺 ⊆ ℂ)
33 xpss12 5605 . . . . . . . . . . . 12 ((ran 𝐹 ⊆ ℂ ∧ ran 𝐺 ⊆ ℂ) → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
3428, 32, 33syl2anc 584 . . . . . . . . . . 11 (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
355fdmi 6610 . . . . . . . . . . 11 dom + = (ℂ × ℂ)
3634, 35sseqtrrdi 3977 . . . . . . . . . 10 (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + )
37 funfvima2 7104 . . . . . . . . . 10 ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
3823, 36, 37sylancr 587 . . . . . . . . 9 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
39 opelxpi 5627 . . . . . . . . 9 ((𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺) → ⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺))
4038, 39impel 506 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺)) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
41 df-ov 7274 . . . . . . . 8 (𝑥 + 𝑦) = ( + ‘⟨𝑥, 𝑦⟩)
424rneqi 5845 . . . . . . . . 9 ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺))
43 df-ima 5603 . . . . . . . . 9 ( + “ (ran 𝐹 × ran 𝐺)) = ran ( + ↾ (ran 𝐹 × ran 𝐺))
4442, 43eqtr4i 2771 . . . . . . . 8 ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺))
4540, 41, 443eltr4g 2858 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ran 𝐹𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃)
4625ffnd 6599 . . . . . . . 8 (𝜑𝐹 Fn ℝ)
47 dffn3 6611 . . . . . . . 8 (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹)
4846, 47sylib 217 . . . . . . 7 (𝜑𝐹:ℝ⟶ran 𝐹)
4930ffnd 6599 . . . . . . . 8 (𝜑𝐺 Fn ℝ)
50 dffn3 6611 . . . . . . . 8 (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺)
5149, 50sylib 217 . . . . . . 7 (𝜑𝐺:ℝ⟶ran 𝐺)
52 reex 10963 . . . . . . . 8 ℝ ∈ V
5352a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ V)
54 inidm 4158 . . . . . . 7 (ℝ ∩ ℝ) = ℝ
5545, 48, 51, 53, 53, 54off 7545 . . . . . 6 (𝜑 → (𝐹f + 𝐺):ℝ⟶ran 𝑃)
5655frnd 6606 . . . . 5 (𝜑 → ran (𝐹f + 𝐺) ⊆ ran 𝑃)
5756ssdifd 4080 . . . 4 (𝜑 → (ran (𝐹f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}))
5826sselda 3926 . . . . . . . . . 10 ((𝜑𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
5931sselda 3926 . . . . . . . . . 10 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
6058, 59anim12dan 619 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
61 readdcl 10955 . . . . . . . . 9 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ)
6260, 61syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ)
6362ralrimivva 3117 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)
64 funimassov 7443 . . . . . . . 8 ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
6523, 36, 64sylancr 587 . . . . . . 7 (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
6663, 65mpbird 256 . . . . . 6 (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ)
6744, 66eqsstrid 3974 . . . . 5 (𝜑 → ran 𝑃 ⊆ ℝ)
6867ssdifd 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 + 𝐺) “ {𝑤}))))
703, 21, 57, 68, 69syl13anc 1371 . . 3 (𝜑 → (∫1‘(𝐹f + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘((𝐹f + 𝐺) “ {𝑤}))))
7130adantr 481 . . . . . . . 8 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ)
7211adantr 481 . . . . . . . 8 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin)
73 inss2 4169 . . . . . . . . 9 ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐺 “ {𝑧})
7473a1i 11 . . . . . . . 8 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐺 “ {𝑧}))
75 i1fima 24840 . . . . . . . . . . 11 (𝐹 ∈ dom ∫1 → (𝐹 “ {(𝑤𝑧)}) ∈ dom vol)
761, 75syl 17 . . . . . . . . . 10 (𝜑 → (𝐹 “ {(𝑤𝑧)}) ∈ dom vol)
77 i1fima 24840 . . . . . . . . . . 11 (𝐺 ∈ dom ∫1 → (𝐺 “ {𝑧}) ∈ dom vol)
782, 77syl 17 . . . . . . . . . 10 (𝜑 → (𝐺 “ {𝑧}) ∈ dom vol)
79 inmbl 24704 . . . . . . . . . 10 (((𝐹 “ {(𝑤𝑧)}) ∈ dom vol ∧ (𝐺 “ {𝑧}) ∈ dom vol) → ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
8076, 78, 79syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
8180ad2antrr 723 . . . . . . . 8 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})) ∈ dom vol)
8219, 67sstrid 3937 . . . . . . . . . . . . 13 (𝜑 → (ran 𝑃 ∖ {0}) ⊆ ℝ)
8382sselda 3926 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ)
8483adantr 481 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ)
8559adantlr 712 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
8684, 85resubcld 11403 . . . . . . . . . 10 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤𝑧) ∈ ℝ)
8784recnd 11004 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ)
8885recnd 11004 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
8987, 88npcand 11336 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧) + 𝑧) = 𝑤)
90 eldifsni 4729 . . . . . . . . . . . . 13 (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0)
9190ad2antlr 724 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0)
9289, 91eqnetrd 3013 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧) + 𝑧) ≠ 0)
93 oveq12 7280 . . . . . . . . . . . . 13 (((𝑤𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤𝑧) + 𝑧) = (0 + 0))
94 00id 11150 . . . . . . . . . . . . 13 (0 + 0) = 0
9593, 94eqtrdi 2796 . . . . . . . . . . . 12 (((𝑤𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤𝑧) + 𝑧) = 0)
9695necon3ai 2970 . . . . . . . . . . 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 24860 . . . . . . . . . 10 ((((𝑤𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤𝑧)𝐼𝑧) = (vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
10086, 85, 97, 99syl21anc 835 . . . . . . . . 9 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧)𝐼𝑧) = (vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
1011, 2, 98itg1addlem2 24859 . . . . . . . . . . 11 (𝜑𝐼:(ℝ × ℝ)⟶ℝ)
102101ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ × ℝ)⟶ℝ)
103102, 86, 85fovrnd 7438 . . . . . . . . 9 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧)𝐼𝑧) ∈ ℝ)
104100, 103eqeltrrd 2842 . . . . . . . 8 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))) ∈ ℝ)
10571, 72, 74, 81, 104itg1addlem1 24854 . . . . . . 7 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘ 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
10683recnd 11004 . . . . . . . . 9 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ)
1071, 2i1faddlem 24855 . . . . . . . . 9 ((𝜑𝑤 ∈ ℂ) → ((𝐹f + 𝐺) “ {𝑤}) = 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})))
108106, 107syldan 591 . . . . . . . 8 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → ((𝐹f + 𝐺) “ {𝑤}) = 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧})))
109108fveq2d 6775 . . . . . . 7 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘((𝐹f + 𝐺) “ {𝑤})) = (vol‘ 𝑧 ∈ ran 𝐺((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
110100sumeq2dv 15413 . . . . . . 7 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((𝐹 “ {(𝑤𝑧)}) ∩ (𝐺 “ {𝑧}))))
111105, 109, 1103eqtr4d 2790 . . . . . 6 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘((𝐹f + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤𝑧)𝐼𝑧))
112111oveq2d 7287 . . . . 5 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘((𝐹f + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤𝑧)𝐼𝑧)))
113103recnd 11004 . . . . . 6 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤𝑧)𝐼𝑧) ∈ ℂ)
11472, 106, 113fsummulc2 15494 . . . . 5 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤𝑧)𝐼𝑧)))
115112, 114eqtrd 2780 . . . 4 ((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘((𝐹f + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤𝑧)𝐼𝑧)))
116115sumeq2dv 15413 . . 3 (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘((𝐹f + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤𝑧)𝐼𝑧)))
11787, 113mulcld 10996 . . . . 5 (((𝜑𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) ∈ ℂ)
118117anasss 467 . . . 4 ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) ∈ ℂ)
11921, 11, 118fsumcom 15485 . . 3 (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)))
12070, 116, 1193eqtrd 2784 . 2 (𝜑 → (∫1‘(𝐹f + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)))
121 oveq1 7278 . . . . . . 7 (𝑦 = (𝑤𝑧) → (𝑦 + 𝑧) = ((𝑤𝑧) + 𝑧))
122 oveq1 7278 . . . . . . 7 (𝑦 = (𝑤𝑧) → (𝑦𝐼𝑧) = ((𝑤𝑧)𝐼𝑧))
123121, 122oveq12d 7289 . . . . . 6 (𝑦 = (𝑤𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤𝑧) + 𝑧) · ((𝑤𝑧)𝐼𝑧)))
12418adantr 481 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin)
12567adantr 481 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ)
126125sselda 3926 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ)
12759adantr 481 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ)
128126, 127resubcld 11403 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣𝑧) ∈ ℝ)
129128ex 413 . . . . . . . 8 ((𝜑𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣𝑧) ∈ ℝ))
130126recnd 11004 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ)
131130adantrr 714 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ)
13267sselda 3926 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ)
133132ad2ant2rl 746 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ)
134133recnd 11004 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ)
13559recnd 11004 . . . . . . . . . . 11 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
136135adantr 481 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ)
137131, 134, 136subcan2ad 11377 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃)) → ((𝑣𝑧) = (𝑦𝑧) ↔ 𝑣 = 𝑦))
138137ex 413 . . . . . . . 8 ((𝜑𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃𝑦 ∈ ran 𝑃) → ((𝑣𝑧) = (𝑦𝑧) ↔ 𝑣 = 𝑦)))
139129, 138dom2lem 8763 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃1-1→ℝ)
140 f1f1orn 6725 . . . . . . 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 7278 . . . . . . . 8 (𝑣 = 𝑤 → (𝑣𝑧) = (𝑤𝑧))
143 eqid 2740 . . . . . . . 8 (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))
144 ovex 7304 . . . . . . . 8 (𝑤𝑧) ∈ V
145142, 143, 144fvmpt 6872 . . . . . . 7 (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))‘𝑤) = (𝑤𝑧))
146145adantl 482 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))‘𝑤) = (𝑤𝑧))
147 f1f 6668 . . . . . . . . . . 11 ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃⟶ℝ)
148 frn 6605 . . . . . . . . . . 11 ((𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ⊆ ℝ)
149139, 147, 1483syl 18 . . . . . . . . . 10 ((𝜑𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ⊆ ℝ)
150149sselda 3926 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → 𝑦 ∈ ℝ)
15159adantr 481 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → 𝑧 ∈ ℝ)
152150, 151readdcld 11005 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → (𝑦 + 𝑧) ∈ ℝ)
153101ad2antrr 723 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → 𝐼:(ℝ × ℝ)⟶ℝ)
154153, 150, 151fovrnd 7438 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → (𝑦𝐼𝑧) ∈ ℝ)
155152, 154remulcld 11006 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
156155recnd 11004 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
157123, 124, 141, 146, 156fsumf1o 15433 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤𝑧) + 𝑧) · ((𝑤𝑧)𝐼𝑧)))
158125sselda 3926 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ)
159158recnd 11004 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ)
160135adantr 481 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ)
161159, 160npcand 11336 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤𝑧) + 𝑧) = 𝑤)
162161oveq1d 7286 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤𝑧) + 𝑧) · ((𝑤𝑧)𝐼𝑧)) = (𝑤 · ((𝑤𝑧)𝐼𝑧)))
163162sumeq2dv 15413 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤𝑧) + 𝑧) · ((𝑤𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤𝑧)𝐼𝑧)))
164157, 163eqtrd 2780 . . . 4 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤𝑧)𝐼𝑧)))
16536ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + )
166 simpr 485 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹)
167 simplr 766 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺)
168166, 167opelxpd 5628 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺))
169 funfvima2 7104 . . . . . . . . . . . 12 ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
17023, 169mpan 687 . . . . . . . . . . 11 ((ran 𝐹 × ran 𝐺) ⊆ dom + → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
171165, 168, 170sylc 65 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
172 df-ov 7274 . . . . . . . . . 10 (𝑦 + 𝑧) = ( + ‘⟨𝑦, 𝑧⟩)
173171, 172, 443eltr4g 2858 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃)
17458adantlr 712 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
175174recnd 11004 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ)
176135adantr 481 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ)
177175, 176pncand 11333 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦)
178177eqcomd 2746 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧))
179 oveq1 7278 . . . . . . . . . 10 (𝑣 = (𝑦 + 𝑧) → (𝑣𝑧) = ((𝑦 + 𝑧) − 𝑧))
180179rspceeqv 3576 . . . . . . . . 9 (((𝑦 + 𝑧) ∈ ran 𝑃𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧))
181173, 178, 180syl2anc 584 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧))
182181ralrimiva 3110 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧))
183 ssabral 4001 . . . . . . 7 (ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧)} ↔ ∀𝑦 ∈ ran 𝐹𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧))
184182, 183sylibr 233 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧)})
185143rnmpt 5863 . . . . . 6 ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣𝑧)}
186184, 185sseqtrrdi 3977 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)))
18759adantr 481 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ)
188174, 187readdcld 11005 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ)
189101ad2antrr 723 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ × ℝ)⟶ℝ)
190189, 174, 187fovrnd 7438 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ)
191188, 190remulcld 11006 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
192191recnd 11004 . . . . 5 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
193149ssdifd 4080 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹))
194193sselda 3926 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹))
195 eldifi 4066 . . . . . . . . . . . . 13 (𝑦 ∈ (ℝ ∖ ran 𝐹) → 𝑦 ∈ ℝ)
196195ad2antrl 725 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ)
19759adantr 481 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ)
198 simprr 770 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0))
1991, 2, 98itg1addlem3 24860 . . . . . . . . . . . 12 (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧}))))
200196, 197, 198, 199syl21anc 835 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧}))))
201 inss1 4168 . . . . . . . . . . . . . . 15 ((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) ⊆ (𝐹 “ {𝑦})
202 eldifn 4067 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (ℝ ∖ ran 𝐹) → ¬ 𝑦 ∈ ran 𝐹)
203202ad2antrl 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹)
204 vex 3435 . . . . . . . . . . . . . . . . . . . . 21 𝑣 ∈ V
205204eliniseg 6001 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ V → (𝑣 ∈ (𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦))
206205elv 3437 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ (𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)
207 vex 3435 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
208204, 207brelrn 5850 . . . . . . . . . . . . . . . . . . 19 (𝑣𝐹𝑦𝑦 ∈ ran 𝐹)
209206, 208sylbi 216 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ (𝐹 “ {𝑦}) → 𝑦 ∈ ran 𝐹)
210203, 209nsyl 140 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑣 ∈ (𝐹 “ {𝑦}))
211210pm2.21d 121 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑣 ∈ (𝐹 “ {𝑦}) → 𝑣 ∈ ∅))
212211ssrdv 3932 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝐹 “ {𝑦}) ⊆ ∅)
213201, 212sstrid 3937 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) ⊆ ∅)
214 ss0 4338 . . . . . . . . . . . . . 14 (((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) ⊆ ∅ → ((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) = ∅)
215213, 214syl 17 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧})) = ∅)
216215fveq2d 6775 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧}))) = (vol‘∅))
217 0mbl 24701 . . . . . . . . . . . . . 14 ∅ ∈ dom vol
218 mblvol 24692 . . . . . . . . . . . . . 14 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
219217, 218ax-mp 5 . . . . . . . . . . . . 13 (vol‘∅) = (vol*‘∅)
220 ovol0 24655 . . . . . . . . . . . . 13 (vol*‘∅) = 0
221219, 220eqtri 2768 . . . . . . . . . . . 12 (vol‘∅) = 0
222216, 221eqtrdi 2796 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((𝐹 “ {𝑦}) ∩ (𝐺 “ {𝑧}))) = 0)
223200, 222eqtrd 2780 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0)
224223oveq2d 7287 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0))
225196, 197readdcld 11005 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ)
226225recnd 11004 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ)
227226mul01d 11174 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0)
228224, 227eqtrd 2780 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
229228expr 457 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0))
230 oveq12 7280 . . . . . . . . . 10 ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0))
231230, 94eqtrdi 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
236234, 98, 235ovmpoa 7422 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0)
237233, 233, 236mp2an 689 . . . . . . . . . 10 (0𝐼0) = 0
238232, 237eqtrdi 2796 . . . . . . . . 9 ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0)
239231, 238oveq12d 7289 . . . . . . . 8 ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0))
240 0cn 10968 . . . . . . . . 9 0 ∈ ℂ
241240mul01i 11165 . . . . . . . 8 (0 · 0) = 0
242239, 241eqtrdi 2796 . . . . . . 7 ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
243229, 242pm2.61d2 181 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
244194, 243syldan 591 . . . . 5 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
245 f1ofo 6721 . . . . . . 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 9083 . . . . . 6 ((ran 𝑃 ∈ Fin ∧ (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)):ran 𝑃onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∈ Fin)
248124, 246, 247syl2anc 584 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧)) ∈ Fin)
249186, 192, 244, 248fsumss 15435 . . . 4 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
25019a1i 11 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃)
251117an32s 649 . . . . 5 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) ∈ ℂ)
252 dfin4 4207 . . . . . . . 8 (ran 𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))
253 inss2 4169 . . . . . . . 8 (ran 𝑃 ∩ {0}) ⊆ {0}
254252, 253eqsstrri 3961 . . . . . . 7 (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆ {0}
255254sseli 3922 . . . . . 6 (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0})
256 elsni 4584 . . . . . . . . 9 (𝑤 ∈ {0} → 𝑤 = 0)
257256adantl 482 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0)
258257oveq1d 7286 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) = (0 · ((𝑤𝑧)𝐼𝑧)))
259101ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ × ℝ)⟶ℝ)
260257, 233eqeltrdi 2849 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ)
26159adantr 481 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ)
262260, 261resubcld 11403 . . . . . . . . . 10 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤𝑧) ∈ ℝ)
263259, 262, 261fovrnd 7438 . . . . . . . . 9 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤𝑧)𝐼𝑧) ∈ ℝ)
264263recnd 11004 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤𝑧)𝐼𝑧) ∈ ℂ)
265264mul02d 11173 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤𝑧)𝐼𝑧)) = 0)
266258, 265eqtrd 2780 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) = 0)
267255, 266sylan2 593 . . . . 5 (((𝜑𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤𝑧)𝐼𝑧)) = 0)
268250, 251, 267, 124fsumss 15435 . . . 4 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤𝑧)𝐼𝑧)))
269164, 249, 2683eqtr4d 2790 . . 3 ((𝜑𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)))
270269sumeq2dv 15413 . 2 (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤𝑧)𝐼𝑧)))
271192anasss 467 . . 3 ((𝜑 ∧ (𝑧 ∈ ran 𝐺𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
27211, 9, 271fsumcom 15485 . 2 (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
273120, 270, 2723eqtr2d 2786 1 (𝜑 → (∫1‘(𝐹f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1542  wcel 2110  {cab 2717  wne 2945  wral 3066  wrex 3067  Vcvv 3431  cdif 3889  cin 3891  wss 3892  c0 4262  ifcif 4465  {csn 4567  cop 4573   ciun 4930   class class class wbr 5079  cmpt 5162   × cxp 5588  ccnv 5589  dom cdm 5590  ran crn 5591  cres 5592  cima 5593  Fun wfun 6426   Fn wfn 6427  wf 6428  1-1wf1 6429  ontowfo 6430  1-1-ontowf1o 6431  cfv 6432  (class class class)co 7271  cmpo 7273  f cof 7525  Fincfn 8716  cc 10870  cr 10871  0cc0 10872   + caddc 10875   · cmul 10877  cmin 11205  Σcsu 15395  vol*covol 24624  volcvol 24625  1citg1 24777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-inf2 9377  ax-cnex 10928  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948  ax-pre-mulgt0 10949  ax-pre-sup 10950  ax-addf 10951
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-int 4886  df-iun 4932  df-disj 5045  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-isom 6441  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-of 7527  df-om 7707  df-1st 7824  df-2nd 7825  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-1o 8288  df-2o 8289  df-er 8481  df-map 8600  df-pm 8601  df-en 8717  df-dom 8718  df-sdom 8719  df-fin 8720  df-sup 9179  df-inf 9180  df-oi 9247  df-dju 9660  df-card 9698  df-pnf 11012  df-mnf 11013  df-xr 11014  df-ltxr 11015  df-le 11016  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-n0 12234  df-z 12320  df-uz 12582  df-q 12688  df-rp 12730  df-xadd 12848  df-ioo 13082  df-ico 13084  df-icc 13085  df-fz 13239  df-fzo 13382  df-fl 13510  df-seq 13720  df-exp 13781  df-hash 14043  df-cj 14808  df-re 14809  df-im 14810  df-sqrt 14944  df-abs 14945  df-clim 15195  df-sum 15396  df-xmet 20588  df-met 20589  df-ovol 24626  df-vol 24627  df-mbf 24781  df-itg1 24782
This theorem is referenced by:  itg1addlem5  24863
  Copyright terms: Public domain W3C validator