Theorem itg1addlem4 24872

Description: Lemma for itg1add 24875. (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.

Step	Hyp	Ref	Expression
1		i1fadd.1	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ dom ∫1)
2		i1fadd.2	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ dom ∫1)
3	1, 2	i1fadd 24868	. . . 4 ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ dom ∫1)
4		itg1add.4	. . . . . . 7 ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))
5		ax-addf 10959	. . . . . . . . 9 ⊢ + :(ℂ × ℂ)⟶ℂ
6		ffn 6609	. . . . . . . . 9 ⊢ ( + :(ℂ × ℂ)⟶ℂ → + Fn (ℂ × ℂ))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ + Fn (ℂ × ℂ)
8		i1frn 24850	. . . . . . . . . 10 ⊢ (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)
9	1, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
10		i1frn 24850	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom ∫1 → ran 𝐺 ∈ Fin)
11	2, 10	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ Fin)
12		xpfi 9094	. . . . . . . . 9 ⊢ ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) → (ran 𝐹 × ran 𝐺) ∈ Fin)
13	9, 11, 12	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin)
14		resfnfinfin 9108	. . . . . . . 8 ⊢ (( + Fn (ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ∈ Fin) → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
15	7, 13, 14	sylancr 587	. . . . . . 7 ⊢ (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
16	4, 15	eqeltrid 2844	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Fin)
17		rnfi 9111	. . . . . 6 ⊢ (𝑃 ∈ Fin → ran 𝑃 ∈ Fin)
18	16, 17	syl 17	. . . . 5 ⊢ (𝜑 → ran 𝑃 ∈ Fin)
19		difss 4067	. . . . 5 ⊢ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃
20		ssfi 8965	. . . . 5 ⊢ ((ran 𝑃 ∈ Fin ∧ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) → (ran 𝑃 ∖ {0}) ∈ Fin)
21	18, 19, 20	sylancl 586	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin)
22		ffun 6612	. . . . . . . . . . 11 ⊢ ( + :(ℂ × ℂ)⟶ℂ → Fun + )
23	5, 22	ax-mp 5	. . . . . . . . . 10 ⊢ Fun +
24		i1ff 24849	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ)
25	1, 24	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
26	25	frnd 6617	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
27		ax-resscn 10937	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
28	26, 27	sstrdi 3934	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐹 ⊆ ℂ)
29		i1ff 24849	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ dom ∫1 → 𝐺:ℝ⟶ℝ)
30	2, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
31	30	frnd 6617	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ⊆ ℝ)
32	31, 27	sstrdi 3934	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 ⊆ ℂ)
33		xpss12 5605	. . . . . . . . . . . 12 ⊢ ((ran 𝐹 ⊆ ℂ ∧ ran 𝐺 ⊆ ℂ) → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
34	28, 32, 33	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
35	5	fdmi 6621	. . . . . . . . . . 11 ⊢ dom + = (ℂ × ℂ)
36	34, 35	sseqtrrdi 3973	. . . . . . . . . 10 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + )
37		funfvima2 7116	. . . . . . . . . 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 7287	. . . . . . . 8 ⊢ (𝑥 + 𝑦) = ( + ‘⟨𝑥, 𝑦⟩)
42	4	rneqi 5849	. . . . . . . . 9 ⊢ ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺))
43		df-ima 5603	. . . . . . . . 9 ⊢ ( + “ (ran 𝐹 × ran 𝐺)) = ran ( + ↾ (ran 𝐹 × ran 𝐺))
44	42, 43	eqtr4i 2770	. . . . . . . 8 ⊢ ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺))
45	40, 41, 44	3eltr4g 2857	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃)
46	25	ffnd 6610	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ℝ)
47		dffn3 6622	. . . . . . . 8 ⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹)
48	46, 47	sylib 217	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹)
49	30	ffnd 6610	. . . . . . . 8 ⊢ (𝜑 → 𝐺 Fn ℝ)
50		dffn3 6622	. . . . . . . 8 ⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺)
51	49, 50	sylib 217	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺)
52		reex 10971	. . . . . . . 8 ⊢ ℝ ∈ V
53	52	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ V)
54		inidm 4153	. . . . . . 7 ⊢ (ℝ ∩ ℝ) = ℝ
55	45, 48, 51, 53, 53, 54	off 7560	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘f + 𝐺):ℝ⟶ran 𝑃)
56	55	frnd 6617	. . . . 5 ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ran 𝑃)
57	56	ssdifd 4076	. . . 4 ⊢ (𝜑 → (ran (𝐹 ∘f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}))
58	26	sselda 3922	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
59	31	sselda 3922	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
60	58, 59	anim12dan 619	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
61		readdcl 10963	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ)
62	60, 61	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ)
63	62	ralrimivva 3124	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)
64		funimassov 7458	. . . . . . . 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 3970	. . . . 5 ⊢ (𝜑 → ran 𝑃 ⊆ ℝ)
68	67	ssdifd 4076	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖ {0}))
69		itg1val2 24857	. . . 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 4164	. . . . . . . . 9 ⊢ ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧})
74	73	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐺 “ {𝑧}))
75		i1fima 24851	. . . . . . . . . . 11 ⊢ (𝐹 ∈ dom ∫1 → (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
76	1, 75	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
77		i1fima 24851	. . . . . . . . . . 11 ⊢ (𝐺 ∈ dom ∫1 → (◡𝐺 “ {𝑧}) ∈ dom vol)
78	2, 77	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (◡𝐺 “ {𝑧}) ∈ dom vol)
79		inmbl 24715	. . . . . . . . . 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 3933	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ ℝ)
83	82	sselda 3922	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ)
84	83	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ)
85	59	adantlr 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
86	84, 85	resubcld 11412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 − 𝑧) ∈ ℝ)
87	84	recnd 11012	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ)
88	85	recnd 11012	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
89	87, 88	npcand 11345	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
90		eldifsni 4724	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0)
91	90	ad2antlr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0)
92	89, 91	eqnetrd 3012	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) ≠ 0)
93		oveq12 7293	. . . . . . . . . . . . 13 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = (0 + 0))
94		00id 11159	. . . . . . . . . . . . 13 ⊢ (0 + 0) = 0
95	93, 94	eqtrdi 2795	. . . . . . . . . . . 12 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = 0)
96	95	necon3ai 2969	. . . . . . . . . . 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 24871	. . . . . . . . . 10 ⊢ ((((𝑤 − 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))))
100	86, 85, 97, 99	syl21anc 835	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))))
101	1, 2, 98	itg1addlem2 24870	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ)
102	101	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ × ℝ)⟶ℝ)
103	102, 86, 85	fovrnd 7453	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
104	100, 103	eqeltrrd 2841	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) ∈ ℝ)
105	71, 72, 74, 81, 104	itg1addlem1 24865	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))))
106	83	recnd 11012	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ)
107	1, 2	i1faddlem 24866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (◡(𝐹 ∘f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))
108	106, 107	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (◡(𝐹 ∘f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧})))
109	108	fveq2d 6787	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤})) = (vol‘∪ 𝑧 ∈ ran 𝐺((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))))
110	100	sumeq2dv 15424	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (◡𝐺 “ {𝑧}))))
111	105, 109, 110	3eqtr4d 2789	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧))
112	111	oveq2d 7300	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)))
113	103	recnd 11012	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
114	72, 106, 113	fsummulc2 15505	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
115	112, 114	eqtrd 2779	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
116	115	sumeq2dv 15424	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(◡(𝐹 ∘f + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
117	87, 113	mulcld 11004	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
118	117	anasss 467	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
119	21, 11, 118	fsumcom 15496	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
120	70, 116, 119	3eqtrd 2783	. 2 ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
121		oveq1 7291	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦 + 𝑧) = ((𝑤 − 𝑧) + 𝑧))
122		oveq1 7291	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦𝐼𝑧) = ((𝑤 − 𝑧)𝐼𝑧))
123	121, 122	oveq12d 7302	. . . . . 6 ⊢ (𝑦 = (𝑤 − 𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
124	18	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin)
125	67	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ)
126	125	sselda 3922	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ)
127	59	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ)
128	126, 127	resubcld 11412	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣 − 𝑧) ∈ ℝ)
129	128	ex 413	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣 − 𝑧) ∈ ℝ))
130	126	recnd 11012	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ)
131	130	adantrr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ)
132	67	sselda 3922	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ)
133	132	ad2ant2rl 746	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ)
134	133	recnd 11012	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ)
135	59	recnd 11012	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
136	135	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ)
137	131, 134, 136	subcan2ad 11386	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦))
138	137	ex 413	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦)))
139	129, 138	dom2lem 8789	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ)
140		f1f1orn 6736	. . . . . . 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 7291	. . . . . . . 8 ⊢ (𝑣 = 𝑤 → (𝑣 − 𝑧) = (𝑤 − 𝑧))
143		eqid 2739	. . . . . . . 8 ⊢ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))
144		ovex 7317	. . . . . . . 8 ⊢ (𝑤 − 𝑧) ∈ V
145	142, 143, 144	fvmpt 6884	. . . . . . 7 ⊢ (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
146	145	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
147		f1f 6679	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ)
148		frn 6616	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
149	139, 147, 148	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
150	149	sselda 3922	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑦 ∈ ℝ)
151	59	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑧 ∈ ℝ)
152	150, 151	readdcld 11013	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦 + 𝑧) ∈ ℝ)
153	101	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝐼:(ℝ × ℝ)⟶ℝ)
154	153, 150, 151	fovrnd 7453	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦𝐼𝑧) ∈ ℝ)
155	152, 154	remulcld 11014	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
156	155	recnd 11012	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
157	123, 124, 141, 146, 156	fsumf1o 15444	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
158	125	sselda 3922	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ)
159	158	recnd 11012	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ)
160	135	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ)
161	159, 160	npcand 11345	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
162	161	oveq1d 7299	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
163	162	sumeq2dv 15424	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
164	157, 163	eqtrd 2779	. . . 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 7116	. . . . . . . . . . . 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 7287	. . . . . . . . . 10 ⊢ (𝑦 + 𝑧) = ( + ‘⟨𝑦, 𝑧⟩)
173	171, 172, 44	3eltr4g 2857	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃)
174	58	adantlr 712	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
175	174	recnd 11012	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ)
176	135	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ)
177	175, 176	pncand 11342	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦)
178	177	eqcomd 2745	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧))
179		oveq1 7291	. . . . . . . . . 10 ⊢ (𝑣 = (𝑦 + 𝑧) → (𝑣 − 𝑧) = ((𝑦 + 𝑧) − 𝑧))
180	179	rspceeqv 3576	. . . . . . . . 9 ⊢ (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
181	173, 178, 180	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
182	181	ralrimiva 3104	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
183		ssabral 3997	. . . . . . 7 ⊢ (ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} ↔ ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
184	182, 183	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)})
185	143	rnmpt 5867	. . . . . 6 ⊢ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)}
186	184, 185	sseqtrrdi 3973	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
187	59	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ)
188	174, 187	readdcld 11013	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ)
189	101	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ × ℝ)⟶ℝ)
190	189, 174, 187	fovrnd 7453	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ)
191	188, 190	remulcld 11014	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
192	191	recnd 11012	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
193	149	ssdifd 4076	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹))
194	193	sselda 3922	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹))
195		eldifi 4062	. . . . . . . . . . . . 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 24871	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))))
200	196, 197, 198, 199	syl21anc 835	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))))
201		inss1 4163	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ (◡𝐹 “ {𝑦})
202		eldifn 4063	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (ℝ ∖ ran 𝐹) → ¬ 𝑦 ∈ ran 𝐹)
203	202	ad2antrl 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹)
204		vex 3437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑣 ∈ V
205	204	eliniseg 6005	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ V → (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦))
206	205	elv 3439	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ (◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)
207		vex 3437	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ V
208	204, 207	brelrn 5854	. . . . . . . . . . . . . . . . . . 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 3928	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (◡𝐹 “ {𝑦}) ⊆ ∅)
213	201, 212	sstrid 3933	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅)
214		ss0 4333	. . . . . . . . . . . . . 14 ⊢ (((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) ⊆ ∅ → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅)
215	213, 214	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧})) = ∅)
216	215	fveq2d 6787	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = (vol‘∅))
217		0mbl 24712	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ dom vol
218		mblvol 24703	. . . . . . . . . . . . . 14 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
219	217, 218	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (vol‘∅) = (vol*‘∅)
220		ovol0 24666	. . . . . . . . . . . . 13 ⊢ (vol*‘∅) = 0
221	219, 220	eqtri 2767	. . . . . . . . . . . 12 ⊢ (vol‘∅) = 0
222	216, 221	eqtrdi 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((◡𝐹 “ {𝑦}) ∩ (◡𝐺 “ {𝑧}))) = 0)
223	200, 222	eqtrd 2779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0)
224	223	oveq2d 7300	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0))
225	196, 197	readdcld 11013	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ)
226	225	recnd 11012	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ)
227	226	mul01d 11183	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0)
228	224, 227	eqtrd 2779	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
229	228	expr 457	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0))
230		oveq12 7293	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0))
231	230, 94	eqtrdi 2795	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0)
232		oveq12 7293	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0))
233		0re 10986	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
234		iftrue 4466	. . . . . . . . . . . 12 ⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) = 0)
235		c0ex 10978	. . . . . . . . . . . 12 ⊢ 0 ∈ V
236	234, 98, 235	ovmpoa 7437	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0)
237	233, 233, 236	mp2an 689	. . . . . . . . . 10 ⊢ (0𝐼0) = 0
238	232, 237	eqtrdi 2795	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0)
239	231, 238	oveq12d 7302	. . . . . . . 8 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0))
240		0cn 10976	. . . . . . . . 9 ⊢ 0 ∈ ℂ
241	240	mul01i 11174	. . . . . . . 8 ⊢ (0 · 0) = 0
242	239, 241	eqtrdi 2795	. . . . . . 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 6732	. . . . . . 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 9114	. . . . . 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 15446	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
250	19	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃)
251	117	an32s 649	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
252		dfin4 4202	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))
253		inss2 4164	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) ⊆ {0}
254	252, 253	eqsstrri 3957	. . . . . . 7 ⊢ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆ {0}
255	254	sseli 3918	. . . . . 6 ⊢ (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0})
256		elsni 4579	. . . . . . . . 9 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
257	256	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0)
258	257	oveq1d 7299	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = (0 · ((𝑤 − 𝑧)𝐼𝑧)))
259	101	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ × ℝ)⟶ℝ)
260	257, 233	eqeltrdi 2848	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ)
261	59	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ)
262	260, 261	resubcld 11412	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 − 𝑧) ∈ ℝ)
263	259, 262, 261	fovrnd 7453	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
264	263	recnd 11012	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
265	264	mul02d 11182	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
266	258, 265	eqtrd 2779	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
267	255, 266	sylan2 593	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
268	250, 251, 267, 124	fsumss 15446	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
269	164, 249, 268	3eqtr4d 2789	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
270	269	sumeq2dv 15424	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
271	192	anasss 467	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
272	11, 9, 271	fsumcom 15496	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
273	120, 270, 272	3eqtr2d 2785	1 ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {cab 2716   ≠ wne 2944  ∀wral 3065  ∃wrex 3066  Vcvv 3433   ∖ cdif 3885   ∩ cin 3887   ⊆ wss 3888  ∅c0 4257  ifcif 4460  {csn 4562  ⟨cop 4568  ∪ ciun 4925   class class class wbr 5075   ↦ cmpt 5158   × cxp 5588  ^◡ccnv 5589  dom cdm 5590  ran crn 5591   ↾ cres 5592   “ cima 5593  Fun wfun 6431   Fn wfn 6432  ⟶wf 6433  –1-1→wf1 6434  –onto→wfo 6435  –1-1-onto→wf1o 6436  ‘cfv 6437  (class class class)co 7284   ∈ cmpo 7286   ∘_f cof 7540  Fincfn 8742  ℂcc 10878  ℝcr 10879  0cc0 10880   + caddc 10883   · cmul 10885   − cmin 11214  Σcsu 15406  vol*covol 24635  volcvol 24636  ∫₁citg1 24788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958  ax-addf 10959

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-disj 5041  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  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 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-er 8507  df-map 8626  df-pm 8627  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-sup 9210  df-inf 9211  df-oi 9278  df-dju 9668  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-n0 12243  df-z 12329  df-uz 12592  df-q 12698  df-rp 12740  df-xadd 12858  df-ioo 13092  df-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-seq 13731  df-exp 13792  df-hash 14054  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-clim 15206  df-sum 15407  df-xmet 20599  df-met 20600  df-ovol 24637  df-vol 24638  df-mbf 24792  df-itg1 24793

This theorem is referenced by:  itg1addlem5  24874