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 24768

Description: Lemma for itg1add 24771. (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 24764	. . . 4 ⊢ (𝜑 → (𝐹 ∘_f + 𝐺) ∈ dom ∫₁)
4		itg1add.4	. . . . . . 7 ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))
5		ax-addf 10881	. . . . . . . . 9 ⊢ + :(ℂ × ℂ)⟶ℂ
6		ffn 6584	. . . . . . . . 9 ⊢ ( + :(ℂ × ℂ)⟶ℂ → + Fn (ℂ × ℂ))
7	5, 6	ax-mp 5	. . . . . . . 8 ⊢ + Fn (ℂ × ℂ)
8		i1frn 24746	. . . . . . . . . 10 ⊢ (𝐹 ∈ dom ∫₁ → ran 𝐹 ∈ Fin)
9	1, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
10		i1frn 24746	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom ∫₁ → ran 𝐺 ∈ Fin)
11	2, 10	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ Fin)
12		xpfi 9015	. . . . . . . . 9 ⊢ ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) → (ran 𝐹 × ran 𝐺) ∈ Fin)
13	9, 11, 12	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin)
14		resfnfinfin 9029	. . . . . . . 8 ⊢ (( + Fn (ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ∈ Fin) → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
15	7, 13, 14	sylancr 586	. . . . . . 7 ⊢ (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) ∈ Fin)
16	4, 15	eqeltrid 2843	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Fin)
17		rnfi 9032	. . . . . 6 ⊢ (𝑃 ∈ Fin → ran 𝑃 ∈ Fin)
18	16, 17	syl 17	. . . . 5 ⊢ (𝜑 → ran 𝑃 ∈ Fin)
19		difss 4062	. . . . 5 ⊢ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃
20		ssfi 8918	. . . . 5 ⊢ ((ran 𝑃 ∈ Fin ∧ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) → (ran 𝑃 ∖ {0}) ∈ Fin)
21	18, 19, 20	sylancl 585	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin)
22		ffun 6587	. . . . . . . . . . 11 ⊢ ( + :(ℂ × ℂ)⟶ℂ → Fun + )
23	5, 22	ax-mp 5	. . . . . . . . . 10 ⊢ Fun +
24		i1ff 24745	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ dom ∫₁ → 𝐹:ℝ⟶ℝ)
25	1, 24	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
26	25	frnd 6592	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
27		ax-resscn 10859	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
28	26, 27	sstrdi 3929	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐹 ⊆ ℂ)
29		i1ff 24745	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ dom ∫₁ → 𝐺:ℝ⟶ℝ)
30	2, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
31	30	frnd 6592	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ⊆ ℝ)
32	31, 27	sstrdi 3929	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 ⊆ ℂ)
33		xpss12 5595	. . . . . . . . . . . 12 ⊢ ((ran 𝐹 ⊆ ℂ ∧ ran 𝐺 ⊆ ℂ) → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
34	28, 32, 33	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
35	5	fdmi 6596	. . . . . . . . . . 11 ⊢ dom + = (ℂ × ℂ)
36	34, 35	sseqtrrdi 3968	. . . . . . . . . 10 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + )
37		funfvima2 7089	. . . . . . . . . 10 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
38	23, 36, 37	sylancr 586	. . . . . . . . 9 ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
39		opelxpi 5617	. . . . . . . . 9 ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺))
40	38, 39	impel 505	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
41		df-ov 7258	. . . . . . . 8 ⊢ (𝑥 + 𝑦) = ( + ‘⟨𝑥, 𝑦⟩)
42	4	rneqi 5835	. . . . . . . . 9 ⊢ ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺))
43		df-ima 5593	. . . . . . . . 9 ⊢ ( + “ (ran 𝐹 × ran 𝐺)) = ran ( + ↾ (ran 𝐹 × ran 𝐺))
44	42, 43	eqtr4i 2769	. . . . . . . 8 ⊢ ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺))
45	40, 41, 44	3eltr4g 2856	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃)
46	25	ffnd 6585	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ℝ)
47		dffn3 6597	. . . . . . . 8 ⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹)
48	46, 47	sylib 217	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹)
49	30	ffnd 6585	. . . . . . . 8 ⊢ (𝜑 → 𝐺 Fn ℝ)
50		dffn3 6597	. . . . . . . 8 ⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺)
51	49, 50	sylib 217	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺)
52		reex 10893	. . . . . . . 8 ⊢ ℝ ∈ V
53	52	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ V)
54		inidm 4149	. . . . . . 7 ⊢ (ℝ ∩ ℝ) = ℝ
55	45, 48, 51, 53, 53, 54	off 7529	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘_f + 𝐺):ℝ⟶ran 𝑃)
56	55	frnd 6592	. . . . 5 ⊢ (𝜑 → ran (𝐹 ∘_f + 𝐺) ⊆ ran 𝑃)
57	56	ssdifd 4071	. . . 4 ⊢ (𝜑 → (ran (𝐹 ∘_f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}))
58	26	sselda 3917	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
59	31	sselda 3917	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
60	58, 59	anim12dan 618	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
61		readdcl 10885	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ)
62	60, 61	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ)
63	62	ralrimivva 3114	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)
64		funimassov 7427	. . . . . . . 8 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
65	23, 36, 64	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
66	63, 65	mpbird 256	. . . . . 6 ⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ)
67	44, 66	eqsstrid 3965	. . . . 5 ⊢ (𝜑 → ran 𝑃 ⊆ ℝ)
68	67	ssdifd 4071	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖ {0}))
69		itg1val2 24753	. . . 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 1370	. . 3 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))))
71	30	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ)
72	11	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin)
73		inss2 4160	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐺 “ {𝑧})
74	73	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐺 “ {𝑧}))
75		i1fima 24747	. . . . . . . . . . 11 ⊢ (𝐹 ∈ dom ∫₁ → (^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
76	1, 75	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
77		i1fima 24747	. . . . . . . . . . 11 ⊢ (𝐺 ∈ dom ∫₁ → (^◡𝐺 “ {𝑧}) ∈ dom vol)
78	2, 77	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐺 “ {𝑧}) ∈ dom vol)
79		inmbl 24611	. . . . . . . . . 10 ⊢ (((^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol ∧ (^◡𝐺 “ {𝑧}) ∈ dom vol) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
80	76, 78, 79	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
81	80	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
82	19, 67	sstrid 3928	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ ℝ)
83	82	sselda 3917	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ)
84	83	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ)
85	59	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
86	84, 85	resubcld 11333	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 − 𝑧) ∈ ℝ)
87	84	recnd 10934	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ)
88	85	recnd 10934	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
89	87, 88	npcand 11266	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
90		eldifsni 4720	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0)
91	90	ad2antlr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0)
92	89, 91	eqnetrd 3010	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) ≠ 0)
93		oveq12 7264	. . . . . . . . . . . . 13 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = (0 + 0))
94		00id 11080	. . . . . . . . . . . . 13 ⊢ (0 + 0) = 0
95	93, 94	eqtrdi 2795	. . . . . . . . . . . 12 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = 0)
96	95	necon3ai 2967	. . . . . . . . . . 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 24767	. . . . . . . . . 10 ⊢ ((((𝑤 − 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
100	86, 85, 97, 99	syl21anc 834	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
101	1, 2, 98	itg1addlem2 24766	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ)
102	101	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ × ℝ)⟶ℝ)
103	102, 86, 85	fovrnd 7422	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
104	100, 103	eqeltrrd 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))) ∈ ℝ)
105	71, 72, 74, 81, 104	itg1addlem1 24761	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
106	83	recnd 10934	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ)
107	1, 2	i1faddlem 24762	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (^◡(𝐹 ∘_f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})))
108	106, 107	syldan 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (^◡(𝐹 ∘_f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})))
109	108	fveq2d 6760	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤})) = (vol‘∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
110	100	sumeq2dv 15343	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
111	105, 109, 110	3eqtr4d 2788	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧))
112	111	oveq2d 7271	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)))
113	103	recnd 10934	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
114	72, 106, 113	fsummulc2 15424	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
115	112, 114	eqtrd 2778	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
116	115	sumeq2dv 15343	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
117	87, 113	mulcld 10926	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
118	117	anasss 466	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
119	21, 11, 118	fsumcom 15415	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
120	70, 116, 119	3eqtrd 2782	. 2 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
121		oveq1 7262	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦 + 𝑧) = ((𝑤 − 𝑧) + 𝑧))
122		oveq1 7262	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦𝐼𝑧) = ((𝑤 − 𝑧)𝐼𝑧))
123	121, 122	oveq12d 7273	. . . . . 6 ⊢ (𝑦 = (𝑤 − 𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
124	18	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin)
125	67	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ)
126	125	sselda 3917	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ)
127	59	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ)
128	126, 127	resubcld 11333	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣 − 𝑧) ∈ ℝ)
129	128	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣 − 𝑧) ∈ ℝ))
130	126	recnd 10934	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ)
131	130	adantrr 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ)
132	67	sselda 3917	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ)
133	132	ad2ant2rl 745	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ)
134	133	recnd 10934	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ)
135	59	recnd 10934	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
136	135	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ)
137	131, 134, 136	subcan2ad 11307	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦))
138	137	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦)))
139	129, 138	dom2lem 8735	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ)
140		f1f1orn 6711	. . . . . . 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 7262	. . . . . . . 8 ⊢ (𝑣 = 𝑤 → (𝑣 − 𝑧) = (𝑤 − 𝑧))
143		eqid 2738	. . . . . . . 8 ⊢ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))
144		ovex 7288	. . . . . . . 8 ⊢ (𝑤 − 𝑧) ∈ V
145	142, 143, 144	fvmpt 6857	. . . . . . 7 ⊢ (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
146	145	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
147		f1f 6654	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ)
148		frn 6591	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
149	139, 147, 148	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
150	149	sselda 3917	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑦 ∈ ℝ)
151	59	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑧 ∈ ℝ)
152	150, 151	readdcld 10935	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦 + 𝑧) ∈ ℝ)
153	101	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝐼:(ℝ × ℝ)⟶ℝ)
154	153, 150, 151	fovrnd 7422	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦𝐼𝑧) ∈ ℝ)
155	152, 154	remulcld 10936	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
156	155	recnd 10934	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
157	123, 124, 141, 146, 156	fsumf1o 15363	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
158	125	sselda 3917	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ)
159	158	recnd 10934	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ)
160	135	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ)
161	159, 160	npcand 11266	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
162	161	oveq1d 7270	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
163	162	sumeq2dv 15343	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
164	157, 163	eqtrd 2778	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
165	36	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + )
166		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹)
167		simplr 765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺)
168	166, 167	opelxpd 5618	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺))
169		funfvima2 7089	. . . . . . . . . . . 12 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
170	23, 169	mpan 686	. . . . . . . . . . 11 ⊢ ((ran 𝐹 × ran 𝐺) ⊆ dom + → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
171	165, 168, 170	sylc 65	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
172		df-ov 7258	. . . . . . . . . 10 ⊢ (𝑦 + 𝑧) = ( + ‘⟨𝑦, 𝑧⟩)
173	171, 172, 44	3eltr4g 2856	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃)
174	58	adantlr 711	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
175	174	recnd 10934	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ)
176	135	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ)
177	175, 176	pncand 11263	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦)
178	177	eqcomd 2744	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧))
179		oveq1 7262	. . . . . . . . . 10 ⊢ (𝑣 = (𝑦 + 𝑧) → (𝑣 − 𝑧) = ((𝑦 + 𝑧) − 𝑧))
180	179	rspceeqv 3567	. . . . . . . . 9 ⊢ (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
181	173, 178, 180	syl2anc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
182	181	ralrimiva 3107	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
183		ssabral 3992	. . . . . . 7 ⊢ (ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} ↔ ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
184	182, 183	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)})
185	143	rnmpt 5853	. . . . . 6 ⊢ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)}
186	184, 185	sseqtrrdi 3968	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
187	59	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ)
188	174, 187	readdcld 10935	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ)
189	101	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ × ℝ)⟶ℝ)
190	189, 174, 187	fovrnd 7422	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ)
191	188, 190	remulcld 10936	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
192	191	recnd 10934	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
193	149	ssdifd 4071	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹))
194	193	sselda 3917	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹))
195		eldifi 4057	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℝ ∖ ran 𝐹) → 𝑦 ∈ ℝ)
196	195	ad2antrl 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ)
197	59	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ)
198		simprr 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0))
199	1, 2, 98	itg1addlem3 24767	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))))
200	196, 197, 198, 199	syl21anc 834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))))
201		inss1 4159	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐹 “ {𝑦})
202		eldifn 4058	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (ℝ ∖ ran 𝐹) → ¬ 𝑦 ∈ ran 𝐹)
203	202	ad2antrl 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹)
204		vex 3426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑣 ∈ V
205	204	eliniseg 5991	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ V → (𝑣 ∈ (^◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦))
206	205	elv 3428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ (^◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)
207		vex 3426	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ V
208	204, 207	brelrn 5840	. . . . . . . . . . . . . . . . . . 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 3923	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (^◡𝐹 “ {𝑦}) ⊆ ∅)
213	201, 212	sstrid 3928	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ ∅)
214		ss0 4329	. . . . . . . . . . . . . 14 ⊢ (((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ ∅ → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) = ∅)
215	213, 214	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) = ∅)
216	215	fveq2d 6760	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))) = (vol‘∅))
217		0mbl 24608	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ dom vol
218		mblvol 24599	. . . . . . . . . . . . . 14 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
219	217, 218	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (vol‘∅) = (vol*‘∅)
220		ovol0 24562	. . . . . . . . . . . . 13 ⊢ (vol*‘∅) = 0
221	219, 220	eqtri 2766	. . . . . . . . . . . 12 ⊢ (vol‘∅) = 0
222	216, 221	eqtrdi 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))) = 0)
223	200, 222	eqtrd 2778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0)
224	223	oveq2d 7271	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0))
225	196, 197	readdcld 10935	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ)
226	225	recnd 10934	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ)
227	226	mul01d 11104	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0)
228	224, 227	eqtrd 2778	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
229	228	expr 456	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0))
230		oveq12 7264	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0))
231	230, 94	eqtrdi 2795	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0)
232		oveq12 7264	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0))
233		0re 10908	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
234		iftrue 4462	. . . . . . . . . . . 12 ⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((^◡𝐹 “ {𝑖}) ∩ (^◡𝐺 “ {𝑗})))) = 0)
235		c0ex 10900	. . . . . . . . . . . 12 ⊢ 0 ∈ V
236	234, 98, 235	ovmpoa 7406	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0)
237	233, 233, 236	mp2an 688	. . . . . . . . . 10 ⊢ (0𝐼0) = 0
238	232, 237	eqtrdi 2795	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0)
239	231, 238	oveq12d 7273	. . . . . . . 8 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0))
240		0cn 10898	. . . . . . . . 9 ⊢ 0 ∈ ℂ
241	240	mul01i 11095	. . . . . . . 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 590	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
245		f1ofo 6707	. . . . . . 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 9035	. . . . . 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 15365	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
250	19	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃)
251	117	an32s 648	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
252		dfin4 4198	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))
253		inss2 4160	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) ⊆ {0}
254	252, 253	eqsstrri 3952	. . . . . . 7 ⊢ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆ {0}
255	254	sseli 3913	. . . . . 6 ⊢ (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0})
256		elsni 4575	. . . . . . . . 9 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
257	256	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0)
258	257	oveq1d 7270	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = (0 · ((𝑤 − 𝑧)𝐼𝑧)))
259	101	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ × ℝ)⟶ℝ)
260	257, 233	eqeltrdi 2847	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ)
261	59	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ)
262	260, 261	resubcld 11333	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 − 𝑧) ∈ ℝ)
263	259, 262, 261	fovrnd 7422	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
264	263	recnd 10934	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
265	264	mul02d 11103	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
266	258, 265	eqtrd 2778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
267	255, 266	sylan2 592	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
268	250, 251, 267, 124	fsumss 15365	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
269	164, 249, 268	3eqtr4d 2788	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
270	269	sumeq2dv 15343	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
271	192	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
272	11, 9, 271	fsumcom 15415	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
273	120, 270, 272	3eqtr2d 2784	1 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 {cab 2715 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 ∖ cdif 3880 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 ifcif 4456 {csn 4558 ⟨cop 4564 ∪ ciun 4921 class class class wbr 5070 ↦ cmpt 5153 × cxp 5578 ^◡ccnv 5579 dom cdm 5580 ran crn 5581 ↾ cres 5582 “ cima 5583 Fun wfun 6412 Fn wfn 6413 ⟶wf 6414 –1-1→wf1 6415 –onto→wfo 6416 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 ∈ cmpo 7257 ∘_f cof 7509 Fincfn 8691 ℂcc 10800 ℝcr 10801 0cc0 10802 + caddc 10805 · cmul 10807 − cmin 11135 Σcsu 15325 vol*covol 24531 volcvol 24532 ∫₁citg1 24684

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-addf 10881

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-disj 5036 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-oi 9199 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-q 12618 df-rp 12660 df-xadd 12778 df-ioo 13012 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125 df-sum 15326 df-xmet 20503 df-met 20504 df-ovol 24533 df-vol 24534 df-mbf 24688 df-itg1 24689

This theorem is referenced by: itg1addlem5 24770

W3C validator