MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg1addlem4 Structured version   Visualization version   GIF version
Theorem itg1addlem4 25550
Description: Lemma for itg1add 25553. (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 25546 . . . 4 (πœ‘ β†’ (𝐹 ∘f + 𝐺) ∈ dom ∫1)
4 itg1add.4 . . . . . . 7 𝑃 = ( + β†Ύ (ran 𝐹 Γ— ran 𝐺))
5 ax-addf 11185 . . . . . . . . 9 + :(β„‚ Γ— β„‚)βŸΆβ„‚
6 ffn 6707 . . . . . . . . 9 ( + :(β„‚ Γ— β„‚)βŸΆβ„‚ β†’ + Fn (β„‚ Γ— β„‚))
75, 6ax-mp 5 . . . . . . . 8 + Fn (β„‚ Γ— β„‚)
8 i1frn 25528 . . . . . . . . . 10 (𝐹 ∈ dom ∫1 β†’ ran 𝐹 ∈ Fin)
91, 8syl 17 . . . . . . . . 9 (πœ‘ β†’ ran 𝐹 ∈ Fin)
10 i1frn 25528 . . . . . . . . . 10 (𝐺 ∈ dom ∫1 β†’ ran 𝐺 ∈ Fin)
112, 10syl 17 . . . . . . . . 9 (πœ‘ β†’ ran 𝐺 ∈ Fin)
12 xpfi 9313 . . . . . . . . 9 ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) β†’ (ran 𝐹 Γ— ran 𝐺) ∈ Fin)
139, 11, 12syl2anc 583 . . . . . . . 8 (πœ‘ β†’ (ran 𝐹 Γ— ran 𝐺) ∈ Fin)
14 resfnfinfin 9328 . . . . . . . 8 (( + Fn (β„‚ Γ— β„‚) ∧ (ran 𝐹 Γ— ran 𝐺) ∈ Fin) β†’ ( + β†Ύ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
157, 13, 14sylancr 586 . . . . . . 7 (πœ‘ β†’ ( + β†Ύ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
164, 15eqeltrid 2829 . . . . . 6 (πœ‘ β†’ 𝑃 ∈ Fin)
17 rnfi 9331 . . . . . 6 (𝑃 ∈ Fin β†’ ran 𝑃 ∈ Fin)
1816, 17syl 17 . . . . 5 (πœ‘ β†’ ran 𝑃 ∈ Fin)
19 difss 4123 . . . . 5 (ran 𝑃 βˆ– {0}) βŠ† ran 𝑃
20 ssfi 9169 . . . . 5 ((ran 𝑃 ∈ Fin ∧ (ran 𝑃 βˆ– {0}) βŠ† ran 𝑃) β†’ (ran 𝑃 βˆ– {0}) ∈ Fin)
2118, 19, 20sylancl 585 . . . 4 (πœ‘ β†’ (ran 𝑃 βˆ– {0}) ∈ Fin)
22 ffun 6710 . . . . . . . . . . 11 ( + :(β„‚ Γ— β„‚)βŸΆβ„‚ β†’ Fun + )
235, 22ax-mp 5 . . . . . . . . . 10 Fun +
24 i1ff 25527 . . . . . . . . . . . . . . 15 (𝐹 ∈ dom ∫1 β†’ 𝐹:β„βŸΆβ„)
251, 24syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
2625frnd 6715 . . . . . . . . . . . . 13 (πœ‘ β†’ ran 𝐹 βŠ† ℝ)
27 ax-resscn 11163 . . . . . . . . . . . . 13 ℝ βŠ† β„‚
2826, 27sstrdi 3986 . . . . . . . . . . . 12 (πœ‘ β†’ ran 𝐹 βŠ† β„‚)
29 i1ff 25527 . . . . . . . . . . . . . . 15 (𝐺 ∈ dom ∫1 β†’ 𝐺:β„βŸΆβ„)
302, 29syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐺:β„βŸΆβ„)
3130frnd 6715 . . . . . . . . . . . . 13 (πœ‘ β†’ ran 𝐺 βŠ† ℝ)
3231, 27sstrdi 3986 . . . . . . . . . . . 12 (πœ‘ β†’ ran 𝐺 βŠ† β„‚)
33 xpss12 5681 . . . . . . . . . . . 12 ((ran 𝐹 βŠ† β„‚ ∧ ran 𝐺 βŠ† β„‚) β†’ (ran 𝐹 Γ— ran 𝐺) βŠ† (β„‚ Γ— β„‚))
3428, 32, 33syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ (ran 𝐹 Γ— ran 𝐺) βŠ† (β„‚ Γ— β„‚))
355fdmi 6719 . . . . . . . . . . 11 dom + = (β„‚ Γ— β„‚)
3634, 35sseqtrrdi 4025 . . . . . . . . . 10 (πœ‘ β†’ (ran 𝐹 Γ— ran 𝐺) βŠ† dom + )
37 funfvima2 7224 . . . . . . . . . 10 ((Fun + ∧ (ran 𝐹 Γ— ran 𝐺) βŠ† dom + ) β†’ (⟨π‘₯, π‘¦βŸ© ∈ (ran 𝐹 Γ— ran 𝐺) β†’ ( + β€˜βŸ¨π‘₯, π‘¦βŸ©) ∈ ( + β€œ (ran 𝐹 Γ— ran 𝐺))))
3823, 36, 37sylancr 586 . . . . . . . . 9 (πœ‘ β†’ (⟨π‘₯, π‘¦βŸ© ∈ (ran 𝐹 Γ— ran 𝐺) β†’ ( + β€˜βŸ¨π‘₯, π‘¦βŸ©) ∈ ( + β€œ (ran 𝐹 Γ— ran 𝐺))))
39 opelxpi 5703 . . . . . . . . 9 ((π‘₯ ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) β†’ ⟨π‘₯, π‘¦βŸ© ∈ (ran 𝐹 Γ— ran 𝐺))
4038, 39impel 505 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) β†’ ( + β€˜βŸ¨π‘₯, π‘¦βŸ©) ∈ ( + β€œ (ran 𝐹 Γ— ran 𝐺)))
41 df-ov 7404 . . . . . . . 8 (π‘₯ + 𝑦) = ( + β€˜βŸ¨π‘₯, π‘¦βŸ©)
424rneqi 5926 . . . . . . . . 9 ran 𝑃 = ran ( + β†Ύ (ran 𝐹 Γ— ran 𝐺))
43 df-ima 5679 . . . . . . . . 9 ( + β€œ (ran 𝐹 Γ— ran 𝐺)) = ran ( + β†Ύ (ran 𝐹 Γ— ran 𝐺))
4442, 43eqtr4i 2755 . . . . . . . 8 ran 𝑃 = ( + β€œ (ran 𝐹 Γ— ran 𝐺))
4540, 41, 443eltr4g 2842 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) β†’ (π‘₯ + 𝑦) ∈ ran 𝑃)
4625ffnd 6708 . . . . . . . 8 (πœ‘ β†’ 𝐹 Fn ℝ)
47 dffn3 6720 . . . . . . . 8 (𝐹 Fn ℝ ↔ 𝐹:β„βŸΆran 𝐹)
4846, 47sylib 217 . . . . . . 7 (πœ‘ β†’ 𝐹:β„βŸΆran 𝐹)
4930ffnd 6708 . . . . . . . 8 (πœ‘ β†’ 𝐺 Fn ℝ)
50 dffn3 6720 . . . . . . . 8 (𝐺 Fn ℝ ↔ 𝐺:β„βŸΆran 𝐺)
5149, 50sylib 217 . . . . . . 7 (πœ‘ β†’ 𝐺:β„βŸΆran 𝐺)
52 reex 11197 . . . . . . . 8 ℝ ∈ V
5352a1i 11 . . . . . . 7 (πœ‘ β†’ ℝ ∈ V)
54 inidm 4210 . . . . . . 7 (ℝ ∩ ℝ) = ℝ
5545, 48, 51, 53, 53, 54off 7681 . . . . . 6 (πœ‘ β†’ (𝐹 ∘f + 𝐺):β„βŸΆran 𝑃)
5655frnd 6715 . . . . 5 (πœ‘ β†’ ran (𝐹 ∘f + 𝐺) βŠ† ran 𝑃)
5756ssdifd 4132 . . . 4 (πœ‘ β†’ (ran (𝐹 ∘f + 𝐺) βˆ– {0}) βŠ† (ran 𝑃 βˆ– {0}))
5826sselda 3974 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑦 ∈ ℝ)
5931sselda 3974 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ 𝑧 ∈ ℝ)
6058, 59anim12dan 618 . . . . . . . . 9 ((πœ‘ ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) β†’ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
61 readdcl 11189 . . . . . . . . 9 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) β†’ (𝑦 + 𝑧) ∈ ℝ)
6260, 61syl 17 . . . . . . . 8 ((πœ‘ ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) β†’ (𝑦 + 𝑧) ∈ ℝ)
6362ralrimivva 3192 . . . . . . 7 (πœ‘ β†’ βˆ€π‘¦ ∈ ran πΉβˆ€π‘§ ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)
64 funimassov 7577 . . . . . . . 8 ((Fun + ∧ (ran 𝐹 Γ— ran 𝐺) βŠ† dom + ) β†’ (( + β€œ (ran 𝐹 Γ— ran 𝐺)) βŠ† ℝ ↔ βˆ€π‘¦ ∈ ran πΉβˆ€π‘§ ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
6523, 36, 64sylancr 586 . . . . . . 7 (πœ‘ β†’ (( + β€œ (ran 𝐹 Γ— ran 𝐺)) βŠ† ℝ ↔ βˆ€π‘¦ ∈ ran πΉβˆ€π‘§ ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
6663, 65mpbird 257 . . . . . 6 (πœ‘ β†’ ( + β€œ (ran 𝐹 Γ— ran 𝐺)) βŠ† ℝ)
6744, 66eqsstrid 4022 . . . . 5 (πœ‘ β†’ ran 𝑃 βŠ† ℝ)
6867ssdifd 4132 . . . 4 (πœ‘ β†’ (ran 𝑃 βˆ– {0}) βŠ† (ℝ βˆ– {0}))
69 itg1val2 25535 . . . 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 1369 . . 3 (πœ‘ β†’ (∫1β€˜(𝐹 ∘f + 𝐺)) = Σ𝑀 ∈ (ran 𝑃 βˆ– {0})(𝑀 Β· (volβ€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑀}))))
7130adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ 𝐺:β„βŸΆβ„)
7211adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ ran 𝐺 ∈ Fin)
73 inss2 4221 . . . . . . . . 9 ((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧})) βŠ† (◑𝐺 β€œ {𝑧})
7473a1i 11 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ ((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧})) βŠ† (◑𝐺 β€œ {𝑧}))
75 i1fima 25529 . . . . . . . . . . 11 (𝐹 ∈ dom ∫1 β†’ (◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∈ dom vol)
761, 75syl 17 . . . . . . . . . 10 (πœ‘ β†’ (◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∈ dom vol)
77 i1fima 25529 . . . . . . . . . . 11 (𝐺 ∈ dom ∫1 β†’ (◑𝐺 β€œ {𝑧}) ∈ dom vol)
782, 77syl 17 . . . . . . . . . 10 (πœ‘ β†’ (◑𝐺 β€œ {𝑧}) ∈ dom vol)
79 inmbl 25393 . . . . . . . . . 10 (((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∈ dom vol ∧ (◑𝐺 β€œ {𝑧}) ∈ dom vol) β†’ ((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧})) ∈ dom vol)
8076, 78, 79syl2anc 583 . . . . . . . . 9 (πœ‘ β†’ ((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧})) ∈ dom vol)
8180ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ ((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧})) ∈ dom vol)
8219, 67sstrid 3985 . . . . . . . . . . . . 13 (πœ‘ β†’ (ran 𝑃 βˆ– {0}) βŠ† ℝ)
8382sselda 3974 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ 𝑀 ∈ ℝ)
8483adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ 𝑀 ∈ ℝ)
8559adantlr 712 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ 𝑧 ∈ ℝ)
8684, 85resubcld 11639 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ (𝑀 βˆ’ 𝑧) ∈ ℝ)
8784recnd 11239 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ 𝑀 ∈ β„‚)
8885recnd 11239 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ 𝑧 ∈ β„‚)
8987, 88npcand 11572 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ ((𝑀 βˆ’ 𝑧) + 𝑧) = 𝑀)
90 eldifsni 4785 . . . . . . . . . . . . 13 (𝑀 ∈ (ran 𝑃 βˆ– {0}) β†’ 𝑀 β‰  0)
9190ad2antlr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ 𝑀 β‰  0)
9289, 91eqnetrd 3000 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ ((𝑀 βˆ’ 𝑧) + 𝑧) β‰  0)
93 oveq12 7410 . . . . . . . . . . . . 13 (((𝑀 βˆ’ 𝑧) = 0 ∧ 𝑧 = 0) β†’ ((𝑀 βˆ’ 𝑧) + 𝑧) = (0 + 0))
94 00id 11386 . . . . . . . . . . . . 13 (0 + 0) = 0
9593, 94eqtrdi 2780 . . . . . . . . . . . 12 (((𝑀 βˆ’ 𝑧) = 0 ∧ 𝑧 = 0) β†’ ((𝑀 βˆ’ 𝑧) + 𝑧) = 0)
9695necon3ai 2957 . . . . . . . . . . 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 25549 . . . . . . . . . 10 ((((𝑀 βˆ’ 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ Β¬ ((𝑀 βˆ’ 𝑧) = 0 ∧ 𝑧 = 0)) β†’ ((𝑀 βˆ’ 𝑧)𝐼𝑧) = (volβ€˜((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧}))))
10086, 85, 97, 99syl21anc 835 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ ((𝑀 βˆ’ 𝑧)𝐼𝑧) = (volβ€˜((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧}))))
1011, 2, 98itg1addlem2 25548 . . . . . . . . . . 11 (πœ‘ β†’ 𝐼:(ℝ Γ— ℝ)βŸΆβ„)
102101ad2antrr 723 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ 𝐼:(ℝ Γ— ℝ)βŸΆβ„)
103102, 86, 85fovcdmd 7572 . . . . . . . . 9 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ ((𝑀 βˆ’ 𝑧)𝐼𝑧) ∈ ℝ)
104100, 103eqeltrrd 2826 . . . . . . . 8 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ (volβ€˜((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧}))) ∈ ℝ)
10571, 72, 74, 81, 104itg1addlem1 25543 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ (volβ€˜βˆͺ 𝑧 ∈ ran 𝐺((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(volβ€˜((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧}))))
10683recnd 11239 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ 𝑀 ∈ β„‚)
1071, 2i1faddlem 25544 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ β„‚) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑀}) = βˆͺ 𝑧 ∈ ran 𝐺((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧})))
108106, 107syldan 590 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑀}) = βˆͺ 𝑧 ∈ ran 𝐺((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧})))
109108fveq2d 6885 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ (volβ€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑀})) = (volβ€˜βˆͺ 𝑧 ∈ ran 𝐺((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧}))))
110100sumeq2dv 15646 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ Σ𝑧 ∈ ran 𝐺((𝑀 βˆ’ 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(volβ€˜((◑𝐹 β€œ {(𝑀 βˆ’ 𝑧)}) ∩ (◑𝐺 β€œ {𝑧}))))
111105, 109, 1103eqtr4d 2774 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ (volβ€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑀})) = Σ𝑧 ∈ ran 𝐺((𝑀 βˆ’ 𝑧)𝐼𝑧))
112111oveq2d 7417 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ (𝑀 Β· (volβ€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑀}))) = (𝑀 Β· Σ𝑧 ∈ ran 𝐺((𝑀 βˆ’ 𝑧)𝐼𝑧)))
113103recnd 11239 . . . . . 6 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ ((𝑀 βˆ’ 𝑧)𝐼𝑧) ∈ β„‚)
11472, 106, 113fsummulc2 15727 . . . . 5 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ (𝑀 Β· Σ𝑧 ∈ ran 𝐺((𝑀 βˆ’ 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
115112, 114eqtrd 2764 . . . 4 ((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ (𝑀 Β· (volβ€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑀}))) = Σ𝑧 ∈ ran 𝐺(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
116115sumeq2dv 15646 . . 3 (πœ‘ β†’ Σ𝑀 ∈ (ran 𝑃 βˆ– {0})(𝑀 Β· (volβ€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑀}))) = Σ𝑀 ∈ (ran 𝑃 βˆ– {0})Σ𝑧 ∈ ran 𝐺(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
11787, 113mulcld 11231 . . . . 5 (((πœ‘ ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) ∧ 𝑧 ∈ ran 𝐺) β†’ (𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) ∈ β„‚)
118117anasss 466 . . . 4 ((πœ‘ ∧ (𝑀 ∈ (ran 𝑃 βˆ– {0}) ∧ 𝑧 ∈ ran 𝐺)) β†’ (𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) ∈ β„‚)
11921, 11, 118fsumcom 15718 . . 3 (πœ‘ β†’ Σ𝑀 ∈ (ran 𝑃 βˆ– {0})Σ𝑧 ∈ ran 𝐺(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑀 ∈ (ran 𝑃 βˆ– {0})(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
12070, 116, 1193eqtrd 2768 . 2 (πœ‘ β†’ (∫1β€˜(𝐹 ∘f + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑀 ∈ (ran 𝑃 βˆ– {0})(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
121 oveq1 7408 . . . . . . 7 (𝑦 = (𝑀 βˆ’ 𝑧) β†’ (𝑦 + 𝑧) = ((𝑀 βˆ’ 𝑧) + 𝑧))
122 oveq1 7408 . . . . . . 7 (𝑦 = (𝑀 βˆ’ 𝑧) β†’ (𝑦𝐼𝑧) = ((𝑀 βˆ’ 𝑧)𝐼𝑧))
123121, 122oveq12d 7419 . . . . . 6 (𝑦 = (𝑀 βˆ’ 𝑧) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = (((𝑀 βˆ’ 𝑧) + 𝑧) Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
12418adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ ran 𝑃 ∈ Fin)
12567adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ ran 𝑃 βŠ† ℝ)
126125sselda 3974 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) β†’ 𝑣 ∈ ℝ)
12759adantr 480 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) β†’ 𝑧 ∈ ℝ)
128126, 127resubcld 11639 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) β†’ (𝑣 βˆ’ 𝑧) ∈ ℝ)
129128ex 412 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ (𝑣 ∈ ran 𝑃 β†’ (𝑣 βˆ’ 𝑧) ∈ ℝ))
130126recnd 11239 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) β†’ 𝑣 ∈ β„‚)
131130adantrr 714 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) β†’ 𝑣 ∈ β„‚)
13267sselda 3974 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ ran 𝑃) β†’ 𝑦 ∈ ℝ)
133132ad2ant2rl 746 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) β†’ 𝑦 ∈ ℝ)
134133recnd 11239 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) β†’ 𝑦 ∈ β„‚)
13559recnd 11239 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ 𝑧 ∈ β„‚)
136135adantr 480 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) β†’ 𝑧 ∈ β„‚)
137131, 134, 136subcan2ad 11613 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) β†’ ((𝑣 βˆ’ 𝑧) = (𝑦 βˆ’ 𝑧) ↔ 𝑣 = 𝑦))
138137ex 412 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) β†’ ((𝑣 βˆ’ 𝑧) = (𝑦 βˆ’ 𝑧) ↔ 𝑣 = 𝑦)))
139129, 138dom2lem 8984 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)):ran 𝑃–1-1→ℝ)
140 f1f1orn 6834 . . . . . . 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 7408 . . . . . . . 8 (𝑣 = 𝑀 β†’ (𝑣 βˆ’ 𝑧) = (𝑀 βˆ’ 𝑧))
143 eqid 2724 . . . . . . . 8 (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))
144 ovex 7434 . . . . . . . 8 (𝑀 βˆ’ 𝑧) ∈ V
145142, 143, 144fvmpt 6988 . . . . . . 7 (𝑀 ∈ ran 𝑃 β†’ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))β€˜π‘€) = (𝑀 βˆ’ 𝑧))
146145adantl 481 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ ran 𝑃) β†’ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))β€˜π‘€) = (𝑀 βˆ’ 𝑧))
147 f1f 6777 . . . . . . . . . . 11 ((𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)):ran 𝑃–1-1→ℝ β†’ (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)):ran π‘ƒβŸΆβ„)
148 frn 6714 . . . . . . . . . . 11 ((𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)):ran π‘ƒβŸΆβ„ β†’ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)) βŠ† ℝ)
149139, 147, 1483syl 18 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)) βŠ† ℝ)
150149sselda 3974 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))) β†’ 𝑦 ∈ ℝ)
15159adantr 480 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))) β†’ 𝑧 ∈ ℝ)
152150, 151readdcld 11240 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))) β†’ (𝑦 + 𝑧) ∈ ℝ)
153101ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))) β†’ 𝐼:(ℝ Γ— ℝ)βŸΆβ„)
154153, 150, 151fovcdmd 7572 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))) β†’ (𝑦𝐼𝑧) ∈ ℝ)
155152, 154remulcld 11241 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) ∈ ℝ)
156155recnd 11239 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) ∈ β„‚)
157123, 124, 141, 146, 156fsumf1o 15666 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = Σ𝑀 ∈ ran 𝑃(((𝑀 βˆ’ 𝑧) + 𝑧) Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
158125sselda 3974 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ ran 𝑃) β†’ 𝑀 ∈ ℝ)
159158recnd 11239 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ ran 𝑃) β†’ 𝑀 ∈ β„‚)
160135adantr 480 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ ran 𝑃) β†’ 𝑧 ∈ β„‚)
161159, 160npcand 11572 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ ran 𝑃) β†’ ((𝑀 βˆ’ 𝑧) + 𝑧) = 𝑀)
162161oveq1d 7416 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ ran 𝑃) β†’ (((𝑀 βˆ’ 𝑧) + 𝑧) Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) = (𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
163162sumeq2dv 15646 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ Σ𝑀 ∈ ran 𝑃(((𝑀 βˆ’ 𝑧) + 𝑧) Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) = Σ𝑀 ∈ ran 𝑃(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
164157, 163eqtrd 2764 . . . 4 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = Σ𝑀 ∈ ran 𝑃(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
16536ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ (ran 𝐹 Γ— ran 𝐺) βŠ† dom + )
166 simpr 484 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑦 ∈ ran 𝐹)
167 simplr 766 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑧 ∈ ran 𝐺)
168166, 167opelxpd 5705 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ βŸ¨π‘¦, π‘§βŸ© ∈ (ran 𝐹 Γ— ran 𝐺))
169 funfvima2 7224 . . . . . . . . . . . 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 7404 . . . . . . . . . 10 (𝑦 + 𝑧) = ( + β€˜βŸ¨π‘¦, π‘§βŸ©)
173171, 172, 443eltr4g 2842 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ (𝑦 + 𝑧) ∈ ran 𝑃)
17458adantlr 712 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑦 ∈ ℝ)
175174recnd 11239 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑦 ∈ β„‚)
176135adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑧 ∈ β„‚)
177175, 176pncand 11569 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ ((𝑦 + 𝑧) βˆ’ 𝑧) = 𝑦)
178177eqcomd 2730 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑦 = ((𝑦 + 𝑧) βˆ’ 𝑧))
179 oveq1 7408 . . . . . . . . . 10 (𝑣 = (𝑦 + 𝑧) β†’ (𝑣 βˆ’ 𝑧) = ((𝑦 + 𝑧) βˆ’ 𝑧))
180179rspceeqv 3625 . . . . . . . . 9 (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) βˆ’ 𝑧)) β†’ βˆƒπ‘£ ∈ ran 𝑃 𝑦 = (𝑣 βˆ’ 𝑧))
181173, 178, 180syl2anc 583 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ βˆƒπ‘£ ∈ ran 𝑃 𝑦 = (𝑣 βˆ’ 𝑧))
182181ralrimiva 3138 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ βˆ€π‘¦ ∈ ran πΉβˆƒπ‘£ ∈ ran 𝑃 𝑦 = (𝑣 βˆ’ 𝑧))
183 ssabral 4051 . . . . . . 7 (ran 𝐹 βŠ† {𝑦 ∣ βˆƒπ‘£ ∈ ran 𝑃 𝑦 = (𝑣 βˆ’ 𝑧)} ↔ βˆ€π‘¦ ∈ ran πΉβˆƒπ‘£ ∈ ran 𝑃 𝑦 = (𝑣 βˆ’ 𝑧))
184182, 183sylibr 233 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ ran 𝐹 βŠ† {𝑦 ∣ βˆƒπ‘£ ∈ ran 𝑃 𝑦 = (𝑣 βˆ’ 𝑧)})
185143rnmpt 5944 . . . . . 6 ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)) = {𝑦 ∣ βˆƒπ‘£ ∈ ran 𝑃 𝑦 = (𝑣 βˆ’ 𝑧)}
186184, 185sseqtrrdi 4025 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ ran 𝐹 βŠ† ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)))
18759adantr 480 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑧 ∈ ℝ)
188174, 187readdcld 11240 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ (𝑦 + 𝑧) ∈ ℝ)
189101ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝐼:(ℝ Γ— ℝ)βŸΆβ„)
190189, 174, 187fovcdmd 7572 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ (𝑦𝐼𝑧) ∈ ℝ)
191188, 190remulcld 11241 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) ∈ ℝ)
192191recnd 11239 . . . . 5 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) ∈ β„‚)
193149ssdifd 4132 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)) βˆ– ran 𝐹) βŠ† (ℝ βˆ– ran 𝐹))
194193sselda 3974 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)) βˆ– ran 𝐹)) β†’ 𝑦 ∈ (ℝ βˆ– ran 𝐹))
195 eldifi 4118 . . . . . . . . . . . . 13 (𝑦 ∈ (ℝ βˆ– ran 𝐹) β†’ 𝑦 ∈ ℝ)
196195ad2antrl 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ 𝑦 ∈ ℝ)
19759adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ 𝑧 ∈ ℝ)
198 simprr 770 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))
1991, 2, 98itg1addlem3 25549 . . . . . . . . . . . 12 (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0)) β†’ (𝑦𝐼𝑧) = (volβ€˜((◑𝐹 β€œ {𝑦}) ∩ (◑𝐺 β€œ {𝑧}))))
200196, 197, 198, 199syl21anc 835 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ (𝑦𝐼𝑧) = (volβ€˜((◑𝐹 β€œ {𝑦}) ∩ (◑𝐺 β€œ {𝑧}))))
201 inss1 4220 . . . . . . . . . . . . . . 15 ((◑𝐹 β€œ {𝑦}) ∩ (◑𝐺 β€œ {𝑧})) βŠ† (◑𝐹 β€œ {𝑦})
202 eldifn 4119 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (ℝ βˆ– ran 𝐹) β†’ Β¬ 𝑦 ∈ ran 𝐹)
203202ad2antrl 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ Β¬ 𝑦 ∈ ran 𝐹)
204 vex 3470 . . . . . . . . . . . . . . . . . . . . 21 𝑣 ∈ V
205204eliniseg 6083 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ V β†’ (𝑣 ∈ (◑𝐹 β€œ {𝑦}) ↔ 𝑣𝐹𝑦))
206205elv 3472 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ (◑𝐹 β€œ {𝑦}) ↔ 𝑣𝐹𝑦)
207 vex 3470 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
208204, 207brelrn 5931 . . . . . . . . . . . . . . . . . . 19 (𝑣𝐹𝑦 β†’ 𝑦 ∈ ran 𝐹)
209206, 208sylbi 216 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ (◑𝐹 β€œ {𝑦}) β†’ 𝑦 ∈ ran 𝐹)
210203, 209nsyl 140 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ Β¬ 𝑣 ∈ (◑𝐹 β€œ {𝑦}))
211210pm2.21d 121 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ (𝑣 ∈ (◑𝐹 β€œ {𝑦}) β†’ 𝑣 ∈ βˆ…))
212211ssrdv 3980 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ (◑𝐹 β€œ {𝑦}) βŠ† βˆ…)
213201, 212sstrid 3985 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ ((◑𝐹 β€œ {𝑦}) ∩ (◑𝐺 β€œ {𝑧})) βŠ† βˆ…)
214 ss0 4390 . . . . . . . . . . . . . 14 (((◑𝐹 β€œ {𝑦}) ∩ (◑𝐺 β€œ {𝑧})) βŠ† βˆ… β†’ ((◑𝐹 β€œ {𝑦}) ∩ (◑𝐺 β€œ {𝑧})) = βˆ…)
215213, 214syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ ((◑𝐹 β€œ {𝑦}) ∩ (◑𝐺 β€œ {𝑧})) = βˆ…)
216215fveq2d 6885 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ (volβ€˜((◑𝐹 β€œ {𝑦}) ∩ (◑𝐺 β€œ {𝑧}))) = (volβ€˜βˆ…))
217 0mbl 25390 . . . . . . . . . . . . . 14 βˆ… ∈ dom vol
218 mblvol 25381 . . . . . . . . . . . . . 14 (βˆ… ∈ dom vol β†’ (volβ€˜βˆ…) = (vol*β€˜βˆ…))
219217, 218ax-mp 5 . . . . . . . . . . . . 13 (volβ€˜βˆ…) = (vol*β€˜βˆ…)
220 ovol0 25344 . . . . . . . . . . . . 13 (vol*β€˜βˆ…) = 0
221219, 220eqtri 2752 . . . . . . . . . . . 12 (volβ€˜βˆ…) = 0
222216, 221eqtrdi 2780 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ (volβ€˜((◑𝐹 β€œ {𝑦}) ∩ (◑𝐺 β€œ {𝑧}))) = 0)
223200, 222eqtrd 2764 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ (𝑦𝐼𝑧) = 0)
224223oveq2d 7417 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) Β· 0))
225196, 197readdcld 11240 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ (𝑦 + 𝑧) ∈ ℝ)
226225recnd 11239 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ (𝑦 + 𝑧) ∈ β„‚)
227226mul01d 11410 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ ((𝑦 + 𝑧) Β· 0) = 0)
228224, 227eqtrd 2764 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ βˆ– ran 𝐹) ∧ Β¬ (𝑦 = 0 ∧ 𝑧 = 0))) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = 0)
229228expr 456 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ βˆ– ran 𝐹)) β†’ (Β¬ (𝑦 = 0 ∧ 𝑧 = 0) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = 0))
230 oveq12 7410 . . . . . . . . . 10 ((𝑦 = 0 ∧ 𝑧 = 0) β†’ (𝑦 + 𝑧) = (0 + 0))
231230, 94eqtrdi 2780 . . . . . . . . 9 ((𝑦 = 0 ∧ 𝑧 = 0) β†’ (𝑦 + 𝑧) = 0)
232 oveq12 7410 . . . . . . . . . 10 ((𝑦 = 0 ∧ 𝑧 = 0) β†’ (𝑦𝐼𝑧) = (0𝐼0))
233 0re 11213 . . . . . . . . . . 11 0 ∈ ℝ
234 iftrue 4526 . . . . . . . . . . . 12 ((𝑖 = 0 ∧ 𝑗 = 0) β†’ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (volβ€˜((◑𝐹 β€œ {𝑖}) ∩ (◑𝐺 β€œ {𝑗})))) = 0)
235 c0ex 11205 . . . . . . . . . . . 12 0 ∈ V
236234, 98, 235ovmpoa 7555 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 0 ∈ ℝ) β†’ (0𝐼0) = 0)
237233, 233, 236mp2an 689 . . . . . . . . . 10 (0𝐼0) = 0
238232, 237eqtrdi 2780 . . . . . . . . 9 ((𝑦 = 0 ∧ 𝑧 = 0) β†’ (𝑦𝐼𝑧) = 0)
239231, 238oveq12d 7419 . . . . . . . 8 ((𝑦 = 0 ∧ 𝑧 = 0) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = (0 Β· 0))
240 0cn 11203 . . . . . . . . 9 0 ∈ β„‚
241240mul01i 11401 . . . . . . . 8 (0 Β· 0) = 0
242239, 241eqtrdi 2780 . . . . . . 7 ((𝑦 = 0 ∧ 𝑧 = 0) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = 0)
243229, 242pm2.61d2 181 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ βˆ– ran 𝐹)) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = 0)
244194, 243syldan 590 . . . . 5 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)) βˆ– ran 𝐹)) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = 0)
245 f1ofo 6830 . . . . . . 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 9334 . . . . . 6 ((ran 𝑃 ∈ Fin ∧ (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)):ran 𝑃–ontoβ†’ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))) β†’ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)) ∈ Fin)
248124, 246, 247syl2anc 583 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧)) ∈ Fin)
249186, 192, 244, 248fsumss 15668 . . . 4 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 βˆ’ 𝑧))((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)))
25019a1i 11 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ (ran 𝑃 βˆ– {0}) βŠ† ran 𝑃)
251117an32s 649 . . . . 5 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ (ran 𝑃 βˆ– {0})) β†’ (𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) ∈ β„‚)
252 dfin4 4259 . . . . . . . 8 (ran 𝑃 ∩ {0}) = (ran 𝑃 βˆ– (ran 𝑃 βˆ– {0}))
253 inss2 4221 . . . . . . . 8 (ran 𝑃 ∩ {0}) βŠ† {0}
254252, 253eqsstrri 4009 . . . . . . 7 (ran 𝑃 βˆ– (ran 𝑃 βˆ– {0})) βŠ† {0}
255254sseli 3970 . . . . . 6 (𝑀 ∈ (ran 𝑃 βˆ– (ran 𝑃 βˆ– {0})) β†’ 𝑀 ∈ {0})
256 elsni 4637 . . . . . . . . 9 (𝑀 ∈ {0} β†’ 𝑀 = 0)
257256adantl 481 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ 𝑀 = 0)
258257oveq1d 7416 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ (𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) = (0 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
259101ad2antrr 723 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ 𝐼:(ℝ Γ— ℝ)βŸΆβ„)
260257, 233eqeltrdi 2833 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ 𝑀 ∈ ℝ)
26159adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ 𝑧 ∈ ℝ)
262260, 261resubcld 11639 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ (𝑀 βˆ’ 𝑧) ∈ ℝ)
263259, 262, 261fovcdmd 7572 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ ((𝑀 βˆ’ 𝑧)𝐼𝑧) ∈ ℝ)
264263recnd 11239 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ ((𝑀 βˆ’ 𝑧)𝐼𝑧) ∈ β„‚)
265264mul02d 11409 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ (0 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) = 0)
266258, 265eqtrd 2764 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ {0}) β†’ (𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) = 0)
267255, 266sylan2 592 . . . . 5 (((πœ‘ ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑀 ∈ (ran 𝑃 βˆ– (ran 𝑃 βˆ– {0}))) β†’ (𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) = 0)
268250, 251, 267, 124fsumss 15668 . . . 4 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ Σ𝑀 ∈ (ran 𝑃 βˆ– {0})(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)) = Σ𝑀 ∈ ran 𝑃(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
269164, 249, 2683eqtr4d 2774 . . 3 ((πœ‘ ∧ 𝑧 ∈ ran 𝐺) β†’ Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = Σ𝑀 ∈ (ran 𝑃 βˆ– {0})(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
270269sumeq2dv 15646 . 2 (πœ‘ β†’ Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑀 ∈ (ran 𝑃 βˆ– {0})(𝑀 Β· ((𝑀 βˆ’ 𝑧)𝐼𝑧)))
271192anasss 466 . . 3 ((πœ‘ ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) β†’ ((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) ∈ β„‚)
27211, 9, 271fsumcom 15718 . 2 (πœ‘ β†’ Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)))
273120, 270, 2723eqtr2d 2770 1 (πœ‘ β†’ (∫1β€˜(𝐹 ∘f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) Β· (𝑦𝐼𝑧)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  {cab 2701   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  Vcvv 3466   βˆ– cdif 3937   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  ifcif 4520  {csn 4620  βŸ¨cop 4626  βˆͺ ciun 4987   class class class wbr 5138   ↦ cmpt 5221   Γ— cxp 5664  β—‘ccnv 5665  dom cdm 5666  ran crn 5667   β†Ύ cres 5668   β€œ cima 5669  Fun wfun 6527   Fn wfn 6528  βŸΆwf 6529  β€“1-1β†’wf1 6530  β€“ontoβ†’wfo 6531  β€“1-1-ontoβ†’wf1o 6532  β€˜cfv 6533  (class class class)co 7401   ∈ cmpo 7403   ∘f cof 7661  Fincfn 8935  β„‚cc 11104  β„cr 11105  0cc0 11106   + caddc 11109   Β· cmul 11111   βˆ’ cmin 11441  Ξ£csu 15629  vol*covol 25313  volcvol 25314  βˆ«1citg1 25466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-disj 5104  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-xadd 13090  df-ioo 13325  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630  df-xmet 21221  df-met 21222  df-ovol 25315  df-vol 25316  df-mbf 25470  df-itg1 25471
This theorem is referenced by:  itg1addlem5  25552
  Copyright terms: Public domain W3C validator