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 25927

Description: Lemma for itg1add 25929. (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 25923	. . . 4 ⊢ (𝜑 → (𝐹 ∘_f + 𝐺) ∈ dom ∫₁)
4		itg1add.4	. . . . . . 7 ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))
5		ax-addf 11203	. . . . . . . . 9 ⊢ + :(ℂ × ℂ)⟶ℂ
6		ffn 6702	. . . . . . . . 9 ⊢ ( + :(ℂ × ℂ)⟶ℂ → + Fn (ℂ × ℂ))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ + Fn (ℂ × ℂ)
8		i1frn 25905	. . . . . . . . . 10 ⊢ (𝐹 ∈ dom ∫₁ → ran 𝐹 ∈ Fin)
9	1, 8	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
10		i1frn 25905	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom ∫₁ → ran 𝐺 ∈ Fin)
11	2, 10	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ Fin)
12		xpfi 9289	. . . . . . . . 9 ⊢ ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) → (ran 𝐹 × ran 𝐺) ∈ Fin)
13	9, 11, 12	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin)
14		resfnfinfin 9304	. . . . . . . 8 ⊢ (( + Fn (ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ∈ Fin) → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
15	7, 13, 14	sylancr 599	. . . . . . 7 ⊢ (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
16	4, 15	eqeltrid 2864	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Fin)
17		rnfi 9307	. . . . . 6 ⊢ (𝑃 ∈ Fin → ran 𝑃 ∈ Fin)
18	16, 17	syl 18	. . . . 5 ⊢ (𝜑 → ran 𝑃 ∈ Fin)
19		difss 4083	. . . . 5 ⊢ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃
20		ssfi 9167	. . . . 5 ⊢ ((ran 𝑃 ∈ Fin ∧ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) → (ran 𝑃 ∖ {0}) ∈ Fin)
21	18, 19, 20	sylancl 598	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin)
22		ffun 6705	. . . . . . . . . . 11 ⊢ ( + :(ℂ × ℂ)⟶ℂ → Fun + )
23	5, 22	ax-mp 5	. . . . . . . . . 10 ⊢ Fun +
24		i1ff 25904	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ dom ∫₁ → 𝐹:ℝ⟶ℝ)
25	1, 24	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
26	25	frnd 6711	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
27		ax-resscn 11181	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
28	26, 27	sstrdi 3943	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐹 ⊆ ℂ)
29		i1ff 25904	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ dom ∫₁ → 𝐺:ℝ⟶ℝ)
30	2, 29	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
31	30	frnd 6711	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ⊆ ℝ)
32	31, 27	sstrdi 3943	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 ⊆ ℂ)
33		xpss12 5670	. . . . . . . . . . . 12 ⊢ ((ran 𝐹 ⊆ ℂ ∧ ran 𝐺 ⊆ ℂ) → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
34	28, 32, 33	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
35	5	fdmi 6714	. . . . . . . . . . 11 ⊢ dom + = (ℂ × ℂ)
36	34, 35	sseqtrrdi 3972	. . . . . . . . . 10 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + )
37		funfvima2 7230	. . . . . . . . . 10 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
38	23, 36, 37	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
39		opelxpi 5692	. . . . . . . . 9 ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺))
40	38, 39	impel 515	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
41		df-ov 7416	. . . . . . . 8 ⊢ (𝑥 + 𝑦) = ( + ‘⟨𝑥, 𝑦⟩)
42	4	rneqi 5921	. . . . . . . . 9 ⊢ ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺))
43		df-ima 5668	. . . . . . . . 9 ⊢ ( + “ (ran 𝐹 × ran 𝐺)) = ran ( + ↾ (ran 𝐹 × ran 𝐺))
44	42, 43	eqtr4i 2786	. . . . . . . 8 ⊢ ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺))
45	40, 41, 44	3eltr4g 2877	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃)
46	25	ffnd 6703	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ℝ)
47		dffn3 6715	. . . . . . . 8 ⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹)
48	46, 47	sylib 221	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹)
49	30	ffnd 6703	. . . . . . . 8 ⊢ (𝜑 → 𝐺 Fn ℝ)
50		dffn3 6715	. . . . . . . 8 ⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺)
51	49, 50	sylib 221	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺)
52		reex 11215	. . . . . . . 8 ⊢ ℝ ∈ V
53	52	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ V)
54		inidm 4172	. . . . . . 7 ⊢ (ℝ ∩ ℝ) = ℝ
55	45, 48, 51, 53, 53, 54	off 7696	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘_f + 𝐺):ℝ⟶ran 𝑃)
56	55	frnd 6711	. . . . 5 ⊢ (𝜑 → ran (𝐹 ∘_f + 𝐺) ⊆ ran 𝑃)
57	56	ssdifd 4092	. . . 4 ⊢ (𝜑 → (ran (𝐹 ∘_f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}))
58	26	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
59	31	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
60	58, 59	anim12dan 631	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
61		readdcl 11207	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ)
62	60, 61	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ)
63	62	ralrimivva 3205	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)
64		funimassov 7591	. . . . . . . 8 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
65	23, 36, 64	sylancr 599	. . . . . . 7 ⊢ (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
66	63, 65	mpbird 260	. . . . . 6 ⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ)
67	44, 66	eqsstrid 3969	. . . . 5 ⊢ (𝜑 → ran 𝑃 ⊆ ℝ)
68	67	ssdifd 4092	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖ {0}))
69		itg1val2 25912	. . . 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 1399	. . 3 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))))
71	30	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ)
72	11	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin)
73		inss2 4183	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐺 “ {𝑧})
74	73	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐺 “ {𝑧}))
75		i1fima 25906	. . . . . . . . . . 11 ⊢ (𝐹 ∈ dom ∫₁ → (^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
76	1, 75	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
77		i1fima 25906	. . . . . . . . . . 11 ⊢ (𝐺 ∈ dom ∫₁ → (^◡𝐺 “ {𝑧}) ∈ dom vol)
78	2, 77	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐺 “ {𝑧}) ∈ dom vol)
79		inmbl 25770	. . . . . . . . . 10 ⊢ (((^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol ∧ (^◡𝐺 “ {𝑧}) ∈ dom vol) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
80	76, 78, 79	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
81	80	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
82	19, 67	sstrid 3942	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ ℝ)
83	82	sselda 3931	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ)
84	83	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ)
85	59	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
86	84, 85	resubcld 11666	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 − 𝑧) ∈ ℝ)
87	84	recnd 11261	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ)
88	85	recnd 11261	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
89	87, 88	npcand 11597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
90		eldifsni 4753	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0)
91	90	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0)
92	89, 91	eqnetrd 3022	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) ≠ 0)
93		oveq12 7422	. . . . . . . . . . . . 13 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = (0 + 0))
94		00id 11409	. . . . . . . . . . . . 13 ⊢ (0 + 0) = 0
95	93, 94	eqtrdi 2811	. . . . . . . . . . . 12 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = 0)
96	95	necon3ai 2980	. . . . . . . . . . 11 ⊢ (((𝑤 − 𝑧) + 𝑧) ≠ 0 → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0))
97	92, 96	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0))
98		itg1add.3	. . . . . . . . . . 11 ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((^◡𝐹 “ {𝑖}) ∩ (^◡𝐺 “ {𝑗})))))
99	1, 2, 98	itg1addlem3 25926	. . . . . . . . . 10 ⊢ ((((𝑤 − 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
100	86, 85, 97, 99	syl21anc 851	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
101	1, 2, 98	itg1addlem2 25925	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ)
102	101	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ × ℝ)⟶ℝ)
103	102, 86, 85	fovcdmd 7586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
104	100, 103	eqeltrrd 2861	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))) ∈ ℝ)
105	71, 72, 74, 81, 104	itg1addlem1 25920	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
106	83	recnd 11261	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ)
107	1, 2	i1faddlem 25921	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (^◡(𝐹 ∘_f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})))
108	106, 107	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (^◡(𝐹 ∘_f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})))
109	108	fveq2d 6882	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤})) = (vol‘∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
110	100	sumeq2dv 15789	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
111	105, 109, 110	3eqtr4d 2805	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧))
112	111	oveq2d 7429	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)))
113	103	recnd 11261	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
114	72, 106, 113	fsummulc2 15870	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
115	112, 114	eqtrd 2795	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
116	115	sumeq2dv 15789	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
117	87, 113	mulcld 11253	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
118	117	anasss 472	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
119	21, 11, 118	fsumcom 15861	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
120	70, 116, 119	3eqtrd 2799	. 2 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
121		oveq1 7420	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦 + 𝑧) = ((𝑤 − 𝑧) + 𝑧))
122		oveq1 7420	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦𝐼𝑧) = ((𝑤 − 𝑧)𝐼𝑧))
123	121, 122	oveq12d 7431	. . . . . 6 ⊢ (𝑦 = (𝑤 − 𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
124	18	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin)
125	67	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ)
126	125	sselda 3931	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ)
127	59	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ)
128	126, 127	resubcld 11666	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣 − 𝑧) ∈ ℝ)
129	128	ex 418	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣 − 𝑧) ∈ ℝ))
130	126	recnd 11261	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ)
131	130	adantrr 730	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ)
132	67	sselda 3931	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ)
133	132	ad2ant2rl 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ)
134	133	recnd 11261	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ)
135	59	recnd 11261	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
136	135	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ)
137	131, 134, 136	subcan2ad 11638	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦))
138	137	ex 418	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦)))
139	129, 138	dom2lem 8998	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ)
140		f1f1orn 6829	. . . . . . 7 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
141	139, 140	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
142		oveq1 7420	. . . . . . . 8 ⊢ (𝑣 = 𝑤 → (𝑣 − 𝑧) = (𝑤 − 𝑧))
143		eqid 2760	. . . . . . . 8 ⊢ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))
144		ovex 7446	. . . . . . . 8 ⊢ (𝑤 − 𝑧) ∈ V
145	142, 143, 144	fvmpt 6986	. . . . . . 7 ⊢ (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
146	145	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
147		f1f 6771	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ)
148		frn 6710	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
149	139, 147, 148	3syl 19	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
150	149	sselda 3931	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑦 ∈ ℝ)
151	59	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑧 ∈ ℝ)
152	150, 151	readdcld 11262	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦 + 𝑧) ∈ ℝ)
153	101	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝐼:(ℝ × ℝ)⟶ℝ)
154	153, 150, 151	fovcdmd 7586	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦𝐼𝑧) ∈ ℝ)
155	152, 154	remulcld 11263	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
156	155	recnd 11261	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
157	123, 124, 141, 146, 156	fsumf1o 15809	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
158	125	sselda 3931	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ)
159	158	recnd 11261	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ)
160	135	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ)
161	159, 160	npcand 11597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
162	161	oveq1d 7428	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
163	162	sumeq2dv 15789	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
164	157, 163	eqtrd 2795	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
165	36	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + )
166		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹)
167		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺)
168	166, 167	opelxpd 5694	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺))
169		funfvima2 7230	. . . . . . . . . . . 12 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
170	23, 169	mpan 703	. . . . . . . . . . 11 ⊢ ((ran 𝐹 × ran 𝐺) ⊆ dom + → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
171	165, 168, 170	sylc 66	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
172		df-ov 7416	. . . . . . . . . 10 ⊢ (𝑦 + 𝑧) = ( + ‘⟨𝑦, 𝑧⟩)
173	171, 172, 44	3eltr4g 2877	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃)
174	58	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
175	174	recnd 11261	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ)
176	135	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ)
177	175, 176	pncand 11594	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦)
178	177	eqcomd 2766	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧))
179		oveq1 7420	. . . . . . . . . 10 ⊢ (𝑣 = (𝑦 + 𝑧) → (𝑣 − 𝑧) = ((𝑦 + 𝑧) − 𝑧))
180	179	rspceeqv 3599	. . . . . . . . 9 ⊢ (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
181	173, 178, 180	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
182	181	ralrimiva 3154	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
183		ssabral 4012	. . . . . . 7 ⊢ (ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} ↔ ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
184	182, 183	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)})
185	143	rnmpt 5941	. . . . . 6 ⊢ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)}
186	184, 185	sseqtrrdi 3972	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
187	59	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ)
188	174, 187	readdcld 11262	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ)
189	101	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ × ℝ)⟶ℝ)
190	189, 174, 187	fovcdmd 7586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ)
191	188, 190	remulcld 11263	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
192	191	recnd 11261	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
193	149	ssdifd 4092	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹))
194	193	sselda 3931	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹))
195		eldifi 4078	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℝ ∖ ran 𝐹) → 𝑦 ∈ ℝ)
196	195	ad2antrl 741	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ)
197	59	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ)
198		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0))
199	1, 2, 98	itg1addlem3 25926	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))))
200	196, 197, 198, 199	syl21anc 851	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))))
201		inss1 4182	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐹 “ {𝑦})
202		eldifn 4079	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (ℝ ∖ ran 𝐹) → ¬ 𝑦 ∈ ran 𝐹)
203	202	ad2antrl 741	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹)
204		vex 3454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑣 ∈ V
205	204	eliniseg 6090	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ V → (𝑣 ∈ (^◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦))
206	205	elv 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ (^◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)
207		vex 3454	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ V
208	204, 207	brelrn 5926	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣𝐹𝑦 → 𝑦 ∈ ran 𝐹)
209	206, 208	sylbi 220	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ (^◡𝐹 “ {𝑦}) → 𝑦 ∈ ran 𝐹)
210	203, 209	nsyl 141	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑣 ∈ (^◡𝐹 “ {𝑦}))
211	210	pm2.21d 122	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑣 ∈ (^◡𝐹 “ {𝑦}) → 𝑣 ∈ ∅))
212	211	ssrdv 3937	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (^◡𝐹 “ {𝑦}) ⊆ ∅)
213	201, 212	sstrid 3942	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ ∅)
214		ss0 4352	. . . . . . . . . . . . . 14 ⊢ (((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ ∅ → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) = ∅)
215	213, 214	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) = ∅)
216	215	fveq2d 6882	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))) = (vol‘∅))
217		0mbl 25767	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ dom vol
218		mblvol 25758	. . . . . . . . . . . . . 14 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
219	217, 218	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (vol‘∅) = (vol*‘∅)
220		ovol0 25721	. . . . . . . . . . . . 13 ⊢ (vol*‘∅) = 0
221	219, 220	eqtri 2783	. . . . . . . . . . . 12 ⊢ (vol‘∅) = 0
222	216, 221	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))) = 0)
223	200, 222	eqtrd 2795	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0)
224	223	oveq2d 7429	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0))
225	196, 197	readdcld 11262	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ)
226	225	recnd 11261	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ)
227	226	mul01d 11433	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0)
228	224, 227	eqtrd 2795	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
229	228	expr 462	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0))
230		oveq12 7422	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0))
231	230, 94	eqtrdi 2811	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0)
232		oveq12 7422	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0))
233		0re 11234	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
234		iftrue 4488	. . . . . . . . . . . 12 ⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((^◡𝐹 “ {𝑖}) ∩ (^◡𝐺 “ {𝑗})))) = 0)
235		c0ex 11224	. . . . . . . . . . . 12 ⊢ 0 ∈ V
236	234, 98, 235	ovmpoa 7568	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0)
237	233, 233, 236	mp2an 705	. . . . . . . . . 10 ⊢ (0𝐼0) = 0
238	232, 237	eqtrdi 2811	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0)
239	231, 238	oveq12d 7431	. . . . . . . 8 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0))
240		0cn 11222	. . . . . . . . 9 ⊢ 0 ∈ ℂ
241	240	mul01i 11424	. . . . . . . 8 ⊢ (0 · 0) = 0
242	239, 241	eqtrdi 2811	. . . . . . 7 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
243	229, 242	pm2.61d2 183	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
244	194, 243	syldan 603	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
245		f1ofo 6825	. . . . . . 7 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
246	141, 245	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
247		fofi 9283	. . . . . 6 ⊢ ((ran 𝑃 ∈ Fin ∧ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin)
248	124, 246, 247	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin)
249	186, 192, 244, 248	fsumss 15811	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
250	19	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃)
251	117	an32s 665	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
252		dfin4 4224	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))
253		inss2 4183	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) ⊆ {0}
254	252, 253	eqsstrri 3978	. . . . . . 7 ⊢ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆ {0}
255	254	sseli 3927	. . . . . 6 ⊢ (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0})
256		elsni 4601	. . . . . . . . 9 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
257	256	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0)
258	257	oveq1d 7428	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = (0 · ((𝑤 − 𝑧)𝐼𝑧)))
259	101	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ × ℝ)⟶ℝ)
260	257, 233	eqeltrdi 2868	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ)
261	59	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ)
262	260, 261	resubcld 11666	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 − 𝑧) ∈ ℝ)
263	259, 262, 261	fovcdmd 7586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
264	263	recnd 11261	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
265	264	mul02d 11432	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
266	258, 265	eqtrd 2795	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
267	255, 266	sylan2 605	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
268	250, 251, 267, 124	fsumss 15811	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
269	164, 249, 268	3eqtr4d 2805	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
270	269	sumeq2dv 15789	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
271	192	anasss 472	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
272	11, 9, 271	fsumcom 15861	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
273	120, 270, 272	3eqtr2d 2801	1 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 {cab 2738 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ∖ cdif 3896 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 ifcif 4482 {csn 4584 ⟨cop 4590 ∪ ciun 4951 class class class wbr 5103 ↦ cmpt 5186 × cxp 5653 ^◡ccnv 5654 dom cdm 5655 ran crn 5656 ↾ cres 5657 “ cima 5658 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 7413 ∈ cmpo 7415 ∘_f cof 7676 Fincfn 8952 ℂcc 11122 ℝcr 11123 0cc0 11124 + caddc 11127 · cmul 11129 − cmin 11465 Σcsu 15773 vol*covol 25690 volcvol 25691 ∫₁citg1 25843

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-inf2 9620 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201 ax-pre-sup 11202 ax-addf 11203

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 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 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7678 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-er 8696 df-map 8828 df-pm 8829 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9906 df-card 9944 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11467 df-neg 11468 df-div 11896 df-nn 12258 df-2 12327 df-3 12328 df-n0 12529 df-z 12616 df-uz 12888 df-q 12998 df-rp 13043 df-xadd 13164 df-ioo 13402 df-ico 13404 df-icc 13405 df-fz 13562 df-fzo 13710 df-fl 13853 df-seq 14066 df-exp 14126 df-hash 14395 df-cj 15186 df-re 15187 df-im 15188 df-sqrt 15322 df-abs 15323 df-clim 15575 df-sum 15774 df-xmet 21578 df-met 21579 df-ovol 25692 df-vol 25693 df-mbf 25847 df-itg1 25848

This theorem is used by: itg1addlem5 25928

W3C validator