itg1addlem4 - Metamath Proof Explorer

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

Theorem itg1addlem4 25753

Description: Lemma for itg1add 25756. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof shortened by SN, 3-Oct-2024.)

**Hypotheses**
Ref	Expression
i1fadd.1	⊢ (𝜑 → 𝐹 ∈ dom ∫₁)
i1fadd.2	⊢ (𝜑 → 𝐺 ∈ dom ∫₁)
itg1add.3	⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((^◡𝐹 “ {𝑖}) ∩ (^◡𝐺 “ {𝑗})))))
itg1add.4	⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))

**Assertion**
Ref	Expression
itg1addlem4	⊢ (𝜑 → (∫₁‘(𝐹 ∘_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 ∫₁)
2		i1fadd.2	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ dom ∫₁)
3	1, 2	i1fadd 25749	. . . 4 ⊢ (𝜑 → (𝐹 ∘_f + 𝐺) ∈ dom ∫₁)
4		itg1add.4	. . . . . . 7 ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))
5		ax-addf 11263	. . . . . . . . 9 ⊢ + :(ℂ × ℂ)⟶ℂ
6		ffn 6747	. . . . . . . . 9 ⊢ ( + :(ℂ × ℂ)⟶ℂ → + Fn (ℂ × ℂ))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ + Fn (ℂ × ℂ)
8		i1frn 25731	. . . . . . . . . 10 ⊢ (𝐹 ∈ dom ∫₁ → ran 𝐹 ∈ Fin)
9	1, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
10		i1frn 25731	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom ∫₁ → ran 𝐺 ∈ Fin)
11	2, 10	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ Fin)
12		xpfi 9386	. . . . . . . . 9 ⊢ ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) → (ran 𝐹 × ran 𝐺) ∈ Fin)
13	9, 11, 12	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin)
14		resfnfinfin 9405	. . . . . . . 8 ⊢ (( + Fn (ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ∈ Fin) → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
15	7, 13, 14	sylancr 586	. . . . . . 7 ⊢ (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
16	4, 15	eqeltrid 2848	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Fin)
17		rnfi 9408	. . . . . 6 ⊢ (𝑃 ∈ Fin → ran 𝑃 ∈ Fin)
18	16, 17	syl 17	. . . . 5 ⊢ (𝜑 → ran 𝑃 ∈ Fin)
19		difss 4159	. . . . 5 ⊢ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃
20		ssfi 9240	. . . . 5 ⊢ ((ran 𝑃 ∈ Fin ∧ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) → (ran 𝑃 ∖ {0}) ∈ Fin)
21	18, 19, 20	sylancl 585	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin)
22		ffun 6750	. . . . . . . . . . 11 ⊢ ( + :(ℂ × ℂ)⟶ℂ → Fun + )
23	5, 22	ax-mp 5	. . . . . . . . . 10 ⊢ Fun +
24		i1ff 25730	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ dom ∫₁ → 𝐹:ℝ⟶ℝ)
25	1, 24	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
26	25	frnd 6755	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
27		ax-resscn 11241	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
28	26, 27	sstrdi 4021	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐹 ⊆ ℂ)
29		i1ff 25730	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ dom ∫₁ → 𝐺:ℝ⟶ℝ)
30	2, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
31	30	frnd 6755	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ⊆ ℝ)
32	31, 27	sstrdi 4021	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 ⊆ ℂ)
33		xpss12 5715	. . . . . . . . . . . 12 ⊢ ((ran 𝐹 ⊆ ℂ ∧ ran 𝐺 ⊆ ℂ) → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
34	28, 32, 33	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
35	5	fdmi 6758	. . . . . . . . . . 11 ⊢ dom + = (ℂ × ℂ)
36	34, 35	sseqtrrdi 4060	. . . . . . . . . 10 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + )
37		funfvima2 7268	. . . . . . . . . 10 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
38	23, 36, 37	sylancr 586	. . . . . . . . 9 ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
39		opelxpi 5737	. . . . . . . . 9 ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺))
40	38, 39	impel 505	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
41		df-ov 7451	. . . . . . . 8 ⊢ (𝑥 + 𝑦) = ( + ‘⟨𝑥, 𝑦⟩)
42	4	rneqi 5962	. . . . . . . . 9 ⊢ ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺))
43		df-ima 5713	. . . . . . . . 9 ⊢ ( + “ (ran 𝐹 × ran 𝐺)) = ran ( + ↾ (ran 𝐹 × ran 𝐺))
44	42, 43	eqtr4i 2771	. . . . . . . 8 ⊢ ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺))
45	40, 41, 44	3eltr4g 2861	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃)
46	25	ffnd 6748	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ℝ)
47		dffn3 6759	. . . . . . . 8 ⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹)
48	46, 47	sylib 218	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹)
49	30	ffnd 6748	. . . . . . . 8 ⊢ (𝜑 → 𝐺 Fn ℝ)
50		dffn3 6759	. . . . . . . 8 ⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺)
51	49, 50	sylib 218	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺)
52		reex 11275	. . . . . . . 8 ⊢ ℝ ∈ V
53	52	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ V)
54		inidm 4248	. . . . . . 7 ⊢ (ℝ ∩ ℝ) = ℝ
55	45, 48, 51, 53, 53, 54	off 7732	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘_f + 𝐺):ℝ⟶ran 𝑃)
56	55	frnd 6755	. . . . 5 ⊢ (𝜑 → ran (𝐹 ∘_f + 𝐺) ⊆ ran 𝑃)
57	56	ssdifd 4168	. . . 4 ⊢ (𝜑 → (ran (𝐹 ∘_f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}))
58	26	sselda 4008	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
59	31	sselda 4008	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
60	58, 59	anim12dan 618	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
61		readdcl 11267	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ)
62	60, 61	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ)
63	62	ralrimivva 3208	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)
64		funimassov 7627	. . . . . . . 8 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
65	23, 36, 64	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
66	63, 65	mpbird 257	. . . . . 6 ⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ)
67	44, 66	eqsstrid 4057	. . . . 5 ⊢ (𝜑 → ran 𝑃 ⊆ ℝ)
68	67	ssdifd 4168	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖ {0}))
69		itg1val2 25738	. . . 4 ⊢ (((𝐹 ∘_f + 𝐺) ∈ dom ∫₁ ∧ ((ran 𝑃 ∖ {0}) ∈ Fin ∧ (ran (𝐹 ∘_f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}) ∧ (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖ {0}))) → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))))
70	3, 21, 57, 68, 69	syl13anc 1372	. . 3 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))))
71	30	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ)
72	11	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin)
73		inss2 4259	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐺 “ {𝑧})
74	73	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐺 “ {𝑧}))
75		i1fima 25732	. . . . . . . . . . 11 ⊢ (𝐹 ∈ dom ∫₁ → (^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
76	1, 75	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
77		i1fima 25732	. . . . . . . . . . 11 ⊢ (𝐺 ∈ dom ∫₁ → (^◡𝐺 “ {𝑧}) ∈ dom vol)
78	2, 77	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐺 “ {𝑧}) ∈ dom vol)
79		inmbl 25596	. . . . . . . . . 10 ⊢ (((^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol ∧ (^◡𝐺 “ {𝑧}) ∈ dom vol) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
80	76, 78, 79	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
81	80	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
82	19, 67	sstrid 4020	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ ℝ)
83	82	sselda 4008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ)
84	83	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ)
85	59	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
86	84, 85	resubcld 11718	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 − 𝑧) ∈ ℝ)
87	84	recnd 11318	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ)
88	85	recnd 11318	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
89	87, 88	npcand 11651	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
90		eldifsni 4815	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0)
91	90	ad2antlr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0)
92	89, 91	eqnetrd 3014	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) ≠ 0)
93		oveq12 7457	. . . . . . . . . . . . 13 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = (0 + 0))
94		00id 11465	. . . . . . . . . . . . 13 ⊢ (0 + 0) = 0
95	93, 94	eqtrdi 2796	. . . . . . . . . . . 12 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = 0)
96	95	necon3ai 2971	. . . . . . . . . . 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 25752	. . . . . . . . . 10 ⊢ ((((𝑤 − 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
100	86, 85, 97, 99	syl21anc 837	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
101	1, 2, 98	itg1addlem2 25751	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ)
102	101	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ × ℝ)⟶ℝ)
103	102, 86, 85	fovcdmd 7622	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
104	100, 103	eqeltrrd 2845	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))) ∈ ℝ)
105	71, 72, 74, 81, 104	itg1addlem1 25746	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
106	83	recnd 11318	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ)
107	1, 2	i1faddlem 25747	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (^◡(𝐹 ∘_f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})))
108	106, 107	syldan 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (^◡(𝐹 ∘_f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})))
109	108	fveq2d 6924	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤})) = (vol‘∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
110	100	sumeq2dv 15750	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
111	105, 109, 110	3eqtr4d 2790	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧))
112	111	oveq2d 7464	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)))
113	103	recnd 11318	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
114	72, 106, 113	fsummulc2 15832	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
115	112, 114	eqtrd 2780	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
116	115	sumeq2dv 15750	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
117	87, 113	mulcld 11310	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
118	117	anasss 466	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
119	21, 11, 118	fsumcom 15823	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
120	70, 116, 119	3eqtrd 2784	. 2 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
121		oveq1 7455	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦 + 𝑧) = ((𝑤 − 𝑧) + 𝑧))
122		oveq1 7455	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦𝐼𝑧) = ((𝑤 − 𝑧)𝐼𝑧))
123	121, 122	oveq12d 7466	. . . . . 6 ⊢ (𝑦 = (𝑤 − 𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
124	18	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin)
125	67	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ)
126	125	sselda 4008	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ)
127	59	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ)
128	126, 127	resubcld 11718	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣 − 𝑧) ∈ ℝ)
129	128	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣 − 𝑧) ∈ ℝ))
130	126	recnd 11318	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ)
131	130	adantrr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ)
132	67	sselda 4008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ)
133	132	ad2ant2rl 748	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ)
134	133	recnd 11318	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ)
135	59	recnd 11318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
136	135	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ)
137	131, 134, 136	subcan2ad 11692	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦))
138	137	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦)))
139	129, 138	dom2lem 9052	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ)
140		f1f1orn 6873	. . . . . . 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 7455	. . . . . . . 8 ⊢ (𝑣 = 𝑤 → (𝑣 − 𝑧) = (𝑤 − 𝑧))
143		eqid 2740	. . . . . . . 8 ⊢ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))
144		ovex 7481	. . . . . . . 8 ⊢ (𝑤 − 𝑧) ∈ V
145	142, 143, 144	fvmpt 7029	. . . . . . 7 ⊢ (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
146	145	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
147		f1f 6817	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ)
148		frn 6754	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
149	139, 147, 148	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
150	149	sselda 4008	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑦 ∈ ℝ)
151	59	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑧 ∈ ℝ)
152	150, 151	readdcld 11319	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦 + 𝑧) ∈ ℝ)
153	101	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝐼:(ℝ × ℝ)⟶ℝ)
154	153, 150, 151	fovcdmd 7622	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦𝐼𝑧) ∈ ℝ)
155	152, 154	remulcld 11320	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
156	155	recnd 11318	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
157	123, 124, 141, 146, 156	fsumf1o 15771	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
158	125	sselda 4008	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ)
159	158	recnd 11318	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ)
160	135	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ)
161	159, 160	npcand 11651	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
162	161	oveq1d 7463	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
163	162	sumeq2dv 15750	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
164	157, 163	eqtrd 2780	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
165	36	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + )
166		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹)
167		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺)
168	166, 167	opelxpd 5739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺))
169		funfvima2 7268	. . . . . . . . . . . 12 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
170	23, 169	mpan 689	. . . . . . . . . . 11 ⊢ ((ran 𝐹 × ran 𝐺) ⊆ dom + → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
171	165, 168, 170	sylc 65	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
172		df-ov 7451	. . . . . . . . . 10 ⊢ (𝑦 + 𝑧) = ( + ‘⟨𝑦, 𝑧⟩)
173	171, 172, 44	3eltr4g 2861	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃)
174	58	adantlr 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
175	174	recnd 11318	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ)
176	135	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ)
177	175, 176	pncand 11648	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦)
178	177	eqcomd 2746	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧))
179		oveq1 7455	. . . . . . . . . 10 ⊢ (𝑣 = (𝑦 + 𝑧) → (𝑣 − 𝑧) = ((𝑦 + 𝑧) − 𝑧))
180	179	rspceeqv 3658	. . . . . . . . 9 ⊢ (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
181	173, 178, 180	syl2anc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
182	181	ralrimiva 3152	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
183		ssabral 4088	. . . . . . 7 ⊢ (ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} ↔ ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
184	182, 183	sylibr 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)})
185	143	rnmpt 5980	. . . . . 6 ⊢ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)}
186	184, 185	sseqtrrdi 4060	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
187	59	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ)
188	174, 187	readdcld 11319	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ)
189	101	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ × ℝ)⟶ℝ)
190	189, 174, 187	fovcdmd 7622	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ)
191	188, 190	remulcld 11320	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
192	191	recnd 11318	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
193	149	ssdifd 4168	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹))
194	193	sselda 4008	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹))
195		eldifi 4154	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℝ ∖ ran 𝐹) → 𝑦 ∈ ℝ)
196	195	ad2antrl 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ)
197	59	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ)
198		simprr 772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0))
199	1, 2, 98	itg1addlem3 25752	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))))
200	196, 197, 198, 199	syl21anc 837	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))))
201		inss1 4258	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐹 “ {𝑦})
202		eldifn 4155	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (ℝ ∖ ran 𝐹) → ¬ 𝑦 ∈ ran 𝐹)
203	202	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹)
204		vex 3492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑣 ∈ V
205	204	eliniseg 6124	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ V → (𝑣 ∈ (^◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦))
206	205	elv 3493	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ (^◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)
207		vex 3492	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ V
208	204, 207	brelrn 5967	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣𝐹𝑦 → 𝑦 ∈ ran 𝐹)
209	206, 208	sylbi 217	. . . . . . . . . . . . . . . . . 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 4014	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (^◡𝐹 “ {𝑦}) ⊆ ∅)
213	201, 212	sstrid 4020	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ ∅)
214		ss0 4425	. . . . . . . . . . . . . 14 ⊢ (((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ ∅ → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) = ∅)
215	213, 214	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) = ∅)
216	215	fveq2d 6924	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))) = (vol‘∅))
217		0mbl 25593	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ dom vol
218		mblvol 25584	. . . . . . . . . . . . . 14 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
219	217, 218	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (vol‘∅) = (vol*‘∅)
220		ovol0 25547	. . . . . . . . . . . . 13 ⊢ (vol*‘∅) = 0
221	219, 220	eqtri 2768	. . . . . . . . . . . 12 ⊢ (vol‘∅) = 0
222	216, 221	eqtrdi 2796	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))) = 0)
223	200, 222	eqtrd 2780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0)
224	223	oveq2d 7464	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0))
225	196, 197	readdcld 11319	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ)
226	225	recnd 11318	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ)
227	226	mul01d 11489	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0)
228	224, 227	eqtrd 2780	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
229	228	expr 456	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0))
230		oveq12 7457	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0))
231	230, 94	eqtrdi 2796	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0)
232		oveq12 7457	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0))
233		0re 11292	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
234		iftrue 4554	. . . . . . . . . . . 12 ⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((^◡𝐹 “ {𝑖}) ∩ (^◡𝐺 “ {𝑗})))) = 0)
235		c0ex 11284	. . . . . . . . . . . 12 ⊢ 0 ∈ V
236	234, 98, 235	ovmpoa 7605	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0)
237	233, 233, 236	mp2an 691	. . . . . . . . . 10 ⊢ (0𝐼0) = 0
238	232, 237	eqtrdi 2796	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0)
239	231, 238	oveq12d 7466	. . . . . . . 8 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0))
240		0cn 11282	. . . . . . . . 9 ⊢ 0 ∈ ℂ
241	240	mul01i 11480	. . . . . . . 8 ⊢ (0 · 0) = 0
242	239, 241	eqtrdi 2796	. . . . . . 7 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
243	229, 242	pm2.61d2 181	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
244	194, 243	syldan 590	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
245		f1ofo 6869	. . . . . . 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 9379	. . . . . 6 ⊢ ((ran 𝑃 ∈ Fin ∧ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin)
248	124, 246, 247	syl2anc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin)
249	186, 192, 244, 248	fsumss 15773	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
250	19	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃)
251	117	an32s 651	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
252		dfin4 4297	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))
253		inss2 4259	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) ⊆ {0}
254	252, 253	eqsstrri 4044	. . . . . . 7 ⊢ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆ {0}
255	254	sseli 4004	. . . . . 6 ⊢ (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0})
256		elsni 4665	. . . . . . . . 9 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
257	256	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0)
258	257	oveq1d 7463	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = (0 · ((𝑤 − 𝑧)𝐼𝑧)))
259	101	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ × ℝ)⟶ℝ)
260	257, 233	eqeltrdi 2852	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ)
261	59	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ)
262	260, 261	resubcld 11718	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 − 𝑧) ∈ ℝ)
263	259, 262, 261	fovcdmd 7622	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
264	263	recnd 11318	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
265	264	mul02d 11488	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
266	258, 265	eqtrd 2780	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
267	255, 266	sylan2 592	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
268	250, 251, 267, 124	fsumss 15773	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
269	164, 249, 268	3eqtr4d 2790	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
270	269	sumeq2dv 15750	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
271	192	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
272	11, 9, 271	fsumcom 15823	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
273	120, 270, 272	3eqtr2d 2786	1 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2108 {cab 2717 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 Vcvv 3488 ∖ cdif 3973 ∩ cin 3975 ⊆ wss 3976 ∅c0 4352 ifcif 4548 {csn 4648 ⟨cop 4654 ∪ ciun 5015 class class class wbr 5166 ↦ cmpt 5249 × cxp 5698 ^◡ccnv 5699 dom cdm 5700 ran crn 5701 ↾ cres 5702 “ cima 5703 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 –1-1→wf1 6570 –onto→wfo 6571 –1-1-onto→wf1o 6572 ‘cfv 6573 (class class class)co 7448 ∈ cmpo 7450 ∘_f cof 7712 Fincfn 9003 ℂcc 11182 ℝcr 11183 0cc0 11184 + caddc 11187 · cmul 11189 − cmin 11520 Σcsu 15734 vol*covol 25516 volcvol 25517 ∫₁citg1 25669

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262 ax-addf 11263

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-disj 5134 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-er 8763 df-map 8886 df-pm 8887 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-sup 9511 df-inf 9512 df-oi 9579 df-dju 9970 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-n0 12554 df-z 12640 df-uz 12904 df-q 13014 df-rp 13058 df-xadd 13176 df-ioo 13411 df-ico 13413 df-icc 13414 df-fz 13568 df-fzo 13712 df-fl 13843 df-seq 14053 df-exp 14113 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-clim 15534 df-sum 15735 df-xmet 21380 df-met 21381 df-ovol 25518 df-vol 25519 df-mbf 25673 df-itg1 25674

This theorem is referenced by: itg1addlem5 25755

W3C validator