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 24294

Description: Lemma for itg1add . (Contributed by Mario Carneiro, 28-Jun-2014.)

**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 24290	. . . 4 ⊢ (𝜑 → (𝐹 ∘_f + 𝐺) ∈ dom ∫₁)
4		i1frn 24272	. . . . . . . 8 ⊢ (𝐹 ∈ dom ∫₁ → ran 𝐹 ∈ Fin)
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
6		i1frn 24272	. . . . . . . 8 ⊢ (𝐺 ∈ dom ∫₁ → ran 𝐺 ∈ Fin)
7	2, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐺 ∈ Fin)
8		xpfi 8783	. . . . . . 7 ⊢ ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) → (ran 𝐹 × ran 𝐺) ∈ Fin)
9	5, 7, 8	syl2anc 586	. . . . . 6 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin)
10		ax-addf 10610	. . . . . . . . . 10 ⊢ + :(ℂ × ℂ)⟶ℂ
11		ffn 6509	. . . . . . . . . 10 ⊢ ( + :(ℂ × ℂ)⟶ℂ → + Fn (ℂ × ℂ))
12	10, 11	ax-mp 5	. . . . . . . . 9 ⊢ + Fn (ℂ × ℂ)
13		i1ff 24271	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ dom ∫₁ → 𝐹:ℝ⟶ℝ)
14	1, 13	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
15	14	frnd 6516	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
16		ax-resscn 10588	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
17	15, 16	sstrdi 3979	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐹 ⊆ ℂ)
18		i1ff 24271	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ dom ∫₁ → 𝐺:ℝ⟶ℝ)
19	2, 18	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)
20	19	frnd 6516	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐺 ⊆ ℝ)
21	20, 16	sstrdi 3979	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐺 ⊆ ℂ)
22		xpss12 5565	. . . . . . . . . 10 ⊢ ((ran 𝐹 ⊆ ℂ ∧ ran 𝐺 ⊆ ℂ) → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
23	17, 21, 22	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ))
24		fnssres 6465	. . . . . . . . 9 ⊢ (( + Fn (ℂ × ℂ) ∧ (ran 𝐹 × ran 𝐺) ⊆ (ℂ × ℂ)) → ( + ↾ (ran 𝐹 × ran 𝐺)) Fn (ran 𝐹 × ran 𝐺))
25	12, 23, 24	sylancr 589	. . . . . . . 8 ⊢ (𝜑 → ( + ↾ (ran 𝐹 × ran 𝐺)) Fn (ran 𝐹 × ran 𝐺))
26		itg1add.4	. . . . . . . . 9 ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))
27	26	fneq1i 6445	. . . . . . . 8 ⊢ (𝑃 Fn (ran 𝐹 × ran 𝐺) ↔ ( + ↾ (ran 𝐹 × ran 𝐺)) Fn (ran 𝐹 × ran 𝐺))
28	25, 27	sylibr 236	. . . . . . 7 ⊢ (𝜑 → 𝑃 Fn (ran 𝐹 × ran 𝐺))
29		dffn4 6591	. . . . . . 7 ⊢ (𝑃 Fn (ran 𝐹 × ran 𝐺) ↔ 𝑃:(ran 𝐹 × ran 𝐺)–onto→ran 𝑃)
30	28, 29	sylib 220	. . . . . 6 ⊢ (𝜑 → 𝑃:(ran 𝐹 × ran 𝐺)–onto→ran 𝑃)
31		fofi 8804	. . . . . 6 ⊢ (((ran 𝐹 × ran 𝐺) ∈ Fin ∧ 𝑃:(ran 𝐹 × ran 𝐺)–onto→ran 𝑃) → ran 𝑃 ∈ Fin)
32	9, 30, 31	syl2anc 586	. . . . 5 ⊢ (𝜑 → ran 𝑃 ∈ Fin)
33		difss 4108	. . . . 5 ⊢ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃
34		ssfi 8732	. . . . 5 ⊢ ((ran 𝑃 ∈ Fin ∧ (ran 𝑃 ∖ {0}) ⊆ ran 𝑃) → (ran 𝑃 ∖ {0}) ∈ Fin)
35	32, 33, 34	sylancl 588	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ∈ Fin)
36		ffun 6512	. . . . . . . . . . 11 ⊢ ( + :(ℂ × ℂ)⟶ℂ → Fun + )
37	10, 36	ax-mp 5	. . . . . . . . . 10 ⊢ Fun +
38	10	fdmi 6519	. . . . . . . . . . 11 ⊢ dom + = (ℂ × ℂ)
39	23, 38	sseqtrrdi 4018	. . . . . . . . . 10 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ⊆ dom + )
40		funfvima2 6987	. . . . . . . . . 10 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
41	37, 39, 40	sylancr 589	. . . . . . . . 9 ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
42		opelxpi 5587	. . . . . . . . 9 ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺) → ⟨𝑥, 𝑦⟩ ∈ (ran 𝐹 × ran 𝐺))
43	41, 42	impel 508	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → ( + ‘⟨𝑥, 𝑦⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
44		df-ov 7153	. . . . . . . 8 ⊢ (𝑥 + 𝑦) = ( + ‘⟨𝑥, 𝑦⟩)
45	26	rneqi 5802	. . . . . . . . 9 ⊢ ran 𝑃 = ran ( + ↾ (ran 𝐹 × ran 𝐺))
46		df-ima 5563	. . . . . . . . 9 ⊢ ( + “ (ran 𝐹 × ran 𝐺)) = ran ( + ↾ (ran 𝐹 × ran 𝐺))
47	45, 46	eqtr4i 2847	. . . . . . . 8 ⊢ ran 𝑃 = ( + “ (ran 𝐹 × ran 𝐺))
48	43, 44, 47	3eltr4g 2930	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺)) → (𝑥 + 𝑦) ∈ ran 𝑃)
49	14	ffnd 6510	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn ℝ)
50		dffn3 6520	. . . . . . . 8 ⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹)
51	49, 50	sylib 220	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹)
52	19	ffnd 6510	. . . . . . . 8 ⊢ (𝜑 → 𝐺 Fn ℝ)
53		dffn3 6520	. . . . . . . 8 ⊢ (𝐺 Fn ℝ ↔ 𝐺:ℝ⟶ran 𝐺)
54	52, 53	sylib 220	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℝ⟶ran 𝐺)
55		reex 10622	. . . . . . . 8 ⊢ ℝ ∈ V
56	55	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ V)
57		inidm 4195	. . . . . . 7 ⊢ (ℝ ∩ ℝ) = ℝ
58	48, 51, 54, 56, 56, 57	off 7418	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘_f + 𝐺):ℝ⟶ran 𝑃)
59	58	frnd 6516	. . . . 5 ⊢ (𝜑 → ran (𝐹 ∘_f + 𝐺) ⊆ ran 𝑃)
60	59	ssdifd 4117	. . . 4 ⊢ (𝜑 → (ran (𝐹 ∘_f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}))
61	15	sselda 3967	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
62	20	sselda 3967	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
63	61, 62	anim12dan 620	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
64		readdcl 10614	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑧) ∈ ℝ)
65	63, 64	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺)) → (𝑦 + 𝑧) ∈ ℝ)
66	65	ralrimivva 3191	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ)
67		funimassov 7319	. . . . . . . 8 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
68	37, 39, 67	sylancr 589	. . . . . . 7 ⊢ (𝜑 → (( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐺(𝑦 + 𝑧) ∈ ℝ))
69	66, 68	mpbird 259	. . . . . 6 ⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ⊆ ℝ)
70	47, 69	eqsstrid 4015	. . . . 5 ⊢ (𝜑 → ran 𝑃 ⊆ ℝ)
71	70	ssdifd 4117	. . . 4 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖ {0}))
72		itg1val2 24279	. . . 4 ⊢ (((𝐹 ∘_f + 𝐺) ∈ dom ∫₁ ∧ ((ran 𝑃 ∖ {0}) ∈ Fin ∧ (ran (𝐹 ∘_f + 𝐺) ∖ {0}) ⊆ (ran 𝑃 ∖ {0}) ∧ (ran 𝑃 ∖ {0}) ⊆ (ℝ ∖ {0}))) → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))))
73	3, 35, 60, 71, 72	syl13anc 1368	. . 3 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))))
74	19	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝐺:ℝ⟶ℝ)
75	7	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → ran 𝐺 ∈ Fin)
76		inss2 4206	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐺 “ {𝑧})
77	76	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐺 “ {𝑧}))
78		i1fima 24273	. . . . . . . . . . 11 ⊢ (𝐹 ∈ dom ∫₁ → (^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
79	1, 78	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol)
80		i1fima 24273	. . . . . . . . . . 11 ⊢ (𝐺 ∈ dom ∫₁ → (^◡𝐺 “ {𝑧}) ∈ dom vol)
81	2, 80	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐺 “ {𝑧}) ∈ dom vol)
82		inmbl 24137	. . . . . . . . . 10 ⊢ (((^◡𝐹 “ {(𝑤 − 𝑧)}) ∈ dom vol ∧ (^◡𝐺 “ {𝑧}) ∈ dom vol) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
83	79, 81, 82	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
84	83	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})) ∈ dom vol)
85	33, 70	sstrid 3978	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran 𝑃 ∖ {0}) ⊆ ℝ)
86	85	sselda 3967	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℝ)
87	86	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℝ)
88	62	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℝ)
89	87, 88	resubcld 11062	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 − 𝑧) ∈ ℝ)
90	87	recnd 10663	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ∈ ℂ)
91	88	recnd 10663	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
92	90, 91	npcand 10995	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
93		eldifsni 4716	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (ran 𝑃 ∖ {0}) → 𝑤 ≠ 0)
94	93	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝑤 ≠ 0)
95	92, 94	eqnetrd 3083	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧) + 𝑧) ≠ 0)
96		oveq12 7159	. . . . . . . . . . . . 13 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = (0 + 0))
97		00id 10809	. . . . . . . . . . . . 13 ⊢ (0 + 0) = 0
98	96, 97	syl6eq 2872	. . . . . . . . . . . 12 ⊢ (((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0) → ((𝑤 − 𝑧) + 𝑧) = 0)
99	98	necon3ai 3041	. . . . . . . . . . 11 ⊢ (((𝑤 − 𝑧) + 𝑧) ≠ 0 → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0))
100	95, 99	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0))
101		itg1add.3	. . . . . . . . . . 11 ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((^◡𝐹 “ {𝑖}) ∩ (^◡𝐺 “ {𝑗})))))
102	1, 2, 101	itg1addlem3 24293	. . . . . . . . . 10 ⊢ ((((𝑤 − 𝑧) ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ ((𝑤 − 𝑧) = 0 ∧ 𝑧 = 0)) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
103	89, 88, 100, 102	syl21anc 835	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) = (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
104	1, 2, 101	itg1addlem2 24292	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ)
105	104	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → 𝐼:(ℝ × ℝ)⟶ℝ)
106	105, 89, 88	fovrnd 7314	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
107	103, 106	eqeltrrd 2914	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))) ∈ ℝ)
108	74, 75, 77, 84, 107	itg1addlem1 24287	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))) = Σ𝑧 ∈ ran 𝐺(vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
109	86	recnd 10663	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → 𝑤 ∈ ℂ)
110	1, 2	i1faddlem 24288	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (^◡(𝐹 ∘_f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})))
111	109, 110	syldan 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (^◡(𝐹 ∘_f + 𝐺) “ {𝑤}) = ∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧})))
112	111	fveq2d 6669	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤})) = (vol‘∪ 𝑧 ∈ ran 𝐺((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
113	103	sumeq2dv 15054	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧) = Σ𝑧 ∈ ran 𝐺(vol‘((^◡𝐹 “ {(𝑤 − 𝑧)}) ∩ (^◡𝐺 “ {𝑧}))))
114	108, 112, 113	3eqtr4d 2866	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤})) = Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧))
115	114	oveq2d 7166	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)))
116	106	recnd 10663	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
117	75, 109, 116	fsummulc2 15133	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · Σ𝑧 ∈ ran 𝐺((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
118	115, 117	eqtrd 2856	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
119	118	sumeq2dv 15054	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · (vol‘(^◡(𝐹 ∘_f + 𝐺) “ {𝑤}))) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
120	90, 116	mulcld 10655	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) ∧ 𝑧 ∈ ran 𝐺) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
121	120	anasss 469	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ (ran 𝑃 ∖ {0}) ∧ 𝑧 ∈ ran 𝐺)) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
122	35, 7, 121	fsumcom 15124	. . 3 ⊢ (𝜑 → Σ𝑤 ∈ (ran 𝑃 ∖ {0})Σ𝑧 ∈ ran 𝐺(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
123	73, 119, 122	3eqtrd 2860	. 2 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
124		oveq1 7157	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦 + 𝑧) = ((𝑤 − 𝑧) + 𝑧))
125		oveq1 7157	. . . . . . 7 ⊢ (𝑦 = (𝑤 − 𝑧) → (𝑦𝐼𝑧) = ((𝑤 − 𝑧)𝐼𝑧))
126	124, 125	oveq12d 7168	. . . . . 6 ⊢ (𝑦 = (𝑤 − 𝑧) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
127	32	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ∈ Fin)
128	70	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝑃 ⊆ ℝ)
129	128	sselda 3967	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℝ)
130	62	adantr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑧 ∈ ℝ)
131	129, 130	resubcld 11062	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → (𝑣 − 𝑧) ∈ ℝ)
132	131	ex 415	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 → (𝑣 − 𝑧) ∈ ℝ))
133	129	recnd 10663	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑣 ∈ ran 𝑃) → 𝑣 ∈ ℂ)
134	133	adantrr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑣 ∈ ℂ)
135	70	sselda 3967	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → 𝑦 ∈ ℝ)
136	135	ad2ant2rl 747	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℝ)
137	136	recnd 10663	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑦 ∈ ℂ)
138	62	recnd 10663	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ℂ)
139	138	adantr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → 𝑧 ∈ ℂ)
140	134, 137, 139	subcan2ad 11036	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃)) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦))
141	140	ex 415	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ((𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃) → ((𝑣 − 𝑧) = (𝑦 − 𝑧) ↔ 𝑣 = 𝑦)))
142	132, 141	dom2lem 8543	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ)
143		f1f1orn 6621	. . . . . . 7 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
144	142, 143	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
145		oveq1 7157	. . . . . . . 8 ⊢ (𝑣 = 𝑤 → (𝑣 − 𝑧) = (𝑤 − 𝑧))
146		eqid 2821	. . . . . . . 8 ⊢ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))
147		ovex 7183	. . . . . . . 8 ⊢ (𝑤 − 𝑧) ∈ V
148	145, 146, 147	fvmpt 6763	. . . . . . 7 ⊢ (𝑤 ∈ ran 𝑃 → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
149	148	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))‘𝑤) = (𝑤 − 𝑧))
150		f1f 6570	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1→ℝ → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ)
151		frn 6515	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃⟶ℝ → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
152	142, 150, 151	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ⊆ ℝ)
153	152	sselda 3967	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑦 ∈ ℝ)
154	62	adantr 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝑧 ∈ ℝ)
155	153, 154	readdcld 10664	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦 + 𝑧) ∈ ℝ)
156	104	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → 𝐼:(ℝ × ℝ)⟶ℝ)
157	156, 153, 154	fovrnd 7314	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → (𝑦𝐼𝑧) ∈ ℝ)
158	155, 157	remulcld 10665	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
159	158	recnd 10663	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
160	126, 127, 144, 149, 159	fsumf1o 15074	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)))
161	128	sselda 3967	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℝ)
162	161	recnd 10663	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑤 ∈ ℂ)
163	138	adantr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → 𝑧 ∈ ℂ)
164	162, 163	npcand 10995	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → ((𝑤 − 𝑧) + 𝑧) = 𝑤)
165	164	oveq1d 7165	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ ran 𝑃) → (((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
166	165	sumeq2dv 15054	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ ran 𝑃(((𝑤 − 𝑧) + 𝑧) · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
167	160, 166	eqtrd 2856	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
168	39	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (ran 𝐹 × ran 𝐺) ⊆ dom + )
169		simpr 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹)
170		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐺)
171	169, 170	opelxpd 5588	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺))
172		funfvima2 6987	. . . . . . . . . . . 12 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ⊆ dom + ) → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
173	37, 172	mpan 688	. . . . . . . . . . 11 ⊢ ((ran 𝐹 × ran 𝐺) ⊆ dom + → (⟨𝑦, 𝑧⟩ ∈ (ran 𝐹 × ran 𝐺) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺))))
174	168, 171, 173	sylc 65	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ( + ‘⟨𝑦, 𝑧⟩) ∈ ( + “ (ran 𝐹 × ran 𝐺)))
175		df-ov 7153	. . . . . . . . . 10 ⊢ (𝑦 + 𝑧) = ( + ‘⟨𝑦, 𝑧⟩)
176	174, 175, 47	3eltr4g 2930	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ran 𝑃)
177	61	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℝ)
178	177	recnd 10663	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ℂ)
179	138	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℂ)
180	178, 179	pncand 10992	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) − 𝑧) = 𝑦)
181	180	eqcomd 2827	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 = ((𝑦 + 𝑧) − 𝑧))
182		oveq1 7157	. . . . . . . . . 10 ⊢ (𝑣 = (𝑦 + 𝑧) → (𝑣 − 𝑧) = ((𝑦 + 𝑧) − 𝑧))
183	182	rspceeqv 3638	. . . . . . . . 9 ⊢ (((𝑦 + 𝑧) ∈ ran 𝑃 ∧ 𝑦 = ((𝑦 + 𝑧) − 𝑧)) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
184	176, 181, 183	syl2anc 586	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
185	184	ralrimiva 3182	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
186		ssabral 4042	. . . . . . 7 ⊢ (ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)} ↔ ∀𝑦 ∈ ran 𝐹∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧))
187	185, 186	sylibr 236	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)})
188	146	rnmpt 5822	. . . . . 6 ⊢ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) = {𝑦 ∣ ∃𝑣 ∈ ran 𝑃 𝑦 = (𝑣 − 𝑧)}
189	187, 188	sseqtrrdi 4018	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran 𝐹 ⊆ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
190	62	adantr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝑧 ∈ ℝ)
191	177, 190	readdcld 10664	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦 + 𝑧) ∈ ℝ)
192	104	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → 𝐼:(ℝ × ℝ)⟶ℝ)
193	192, 177, 190	fovrnd 7314	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → (𝑦𝐼𝑧) ∈ ℝ)
194	191, 193	remulcld 10665	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℝ)
195	194	recnd 10663	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ ran 𝐹) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
196	152	ssdifd 4117	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹) ⊆ (ℝ ∖ ran 𝐹))
197	196	sselda 3967	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → 𝑦 ∈ (ℝ ∖ ran 𝐹))
198		eldifi 4103	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (ℝ ∖ ran 𝐹) → 𝑦 ∈ ℝ)
199	198	ad2antrl 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑦 ∈ ℝ)
200	62	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → 𝑧 ∈ ℝ)
201		simprr 771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ (𝑦 = 0 ∧ 𝑧 = 0))
202	1, 2, 101	itg1addlem3 24293	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0)) → (𝑦𝐼𝑧) = (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))))
203	199, 200, 201, 202	syl21anc 835	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))))
204		inss1 4205	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ (^◡𝐹 “ {𝑦})
205		eldifn 4104	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (ℝ ∖ ran 𝐹) → ¬ 𝑦 ∈ ran 𝐹)
206	205	ad2antrl 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑦 ∈ ran 𝐹)
207		vex 3498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑣 ∈ V
208	207	eliniseg 5953	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ V → (𝑣 ∈ (^◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦))
209	208	elv 3500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ (^◡𝐹 “ {𝑦}) ↔ 𝑣𝐹𝑦)
210		vex 3498	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ V
211	207, 210	brelrn 5807	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣𝐹𝑦 → 𝑦 ∈ ran 𝐹)
212	209, 211	sylbi 219	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ (^◡𝐹 “ {𝑦}) → 𝑦 ∈ ran 𝐹)
213	206, 212	nsyl 142	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ¬ 𝑣 ∈ (^◡𝐹 “ {𝑦}))
214	213	pm2.21d 121	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑣 ∈ (^◡𝐹 “ {𝑦}) → 𝑣 ∈ ∅))
215	214	ssrdv 3973	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (^◡𝐹 “ {𝑦}) ⊆ ∅)
216	204, 215	sstrid 3978	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ ∅)
217		ss0 4352	. . . . . . . . . . . . . 14 ⊢ (((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) ⊆ ∅ → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) = ∅)
218	216, 217	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧})) = ∅)
219	218	fveq2d 6669	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))) = (vol‘∅))
220		0mbl 24134	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ dom vol
221		mblvol 24125	. . . . . . . . . . . . . 14 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
222	220, 221	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (vol‘∅) = (vol*‘∅)
223		ovol0 24088	. . . . . . . . . . . . 13 ⊢ (vol*‘∅) = 0
224	222, 223	eqtri 2844	. . . . . . . . . . . 12 ⊢ (vol‘∅) = 0
225	219, 224	syl6eq 2872	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (vol‘((^◡𝐹 “ {𝑦}) ∩ (^◡𝐺 “ {𝑧}))) = 0)
226	203, 225	eqtrd 2856	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦𝐼𝑧) = 0)
227	226	oveq2d 7166	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = ((𝑦 + 𝑧) · 0))
228	199, 200	readdcld 10664	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℝ)
229	228	recnd 10663	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → (𝑦 + 𝑧) ∈ ℂ)
230	229	mul01d 10833	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · 0) = 0)
231	227, 230	eqtrd 2856	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ (𝑦 ∈ (ℝ ∖ ran 𝐹) ∧ ¬ (𝑦 = 0 ∧ 𝑧 = 0))) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
232	231	expr 459	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → (¬ (𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0))
233		oveq12 7159	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = (0 + 0))
234	233, 97	syl6eq 2872	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦 + 𝑧) = 0)
235		oveq12 7159	. . . . . . . . . 10 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = (0𝐼0))
236		0re 10637	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
237		iftrue 4473	. . . . . . . . . . . 12 ⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((^◡𝐹 “ {𝑖}) ∩ (^◡𝐺 “ {𝑗})))) = 0)
238		c0ex 10629	. . . . . . . . . . . 12 ⊢ 0 ∈ V
239	237, 101, 238	ovmpoa 7299	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → (0𝐼0) = 0)
240	236, 236, 239	mp2an 690	. . . . . . . . . 10 ⊢ (0𝐼0) = 0
241	235, 240	syl6eq 2872	. . . . . . . . 9 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → (𝑦𝐼𝑧) = 0)
242	234, 241	oveq12d 7168	. . . . . . . 8 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = (0 · 0))
243		0cn 10627	. . . . . . . . 9 ⊢ 0 ∈ ℂ
244	243	mul01i 10824	. . . . . . . 8 ⊢ (0 · 0) = 0
245	242, 244	syl6eq 2872	. . . . . . 7 ⊢ ((𝑦 = 0 ∧ 𝑧 = 0) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
246	232, 245	pm2.61d2 183	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ℝ ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
247	197, 246	syldan 593	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑦 ∈ (ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∖ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = 0)
248		f1ofo 6617	. . . . . . 7 ⊢ ((𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–1-1-onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
249	144, 248	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)))
250		fofi 8804	. . . . . 6 ⊢ ((ran 𝑃 ∈ Fin ∧ (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)):ran 𝑃–onto→ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin)
251	127, 249, 250	syl2anc 586	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧)) ∈ Fin)
252	189, 195, 247, 251	fsumss 15076	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran (𝑣 ∈ ran 𝑃 ↦ (𝑣 − 𝑧))((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
253	33	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (ran 𝑃 ∖ {0}) ⊆ ran 𝑃)
254	120	an32s 650	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ {0})) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) ∈ ℂ)
255		dfin4 4244	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) = (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))
256		inss2 4206	. . . . . . . 8 ⊢ (ran 𝑃 ∩ {0}) ⊆ {0}
257	255, 256	eqsstrri 4002	. . . . . . 7 ⊢ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) ⊆ {0}
258	257	sseli 3963	. . . . . 6 ⊢ (𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0})) → 𝑤 ∈ {0})
259		elsni 4578	. . . . . . . . 9 ⊢ (𝑤 ∈ {0} → 𝑤 = 0)
260	259	adantl 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 = 0)
261	260	oveq1d 7165	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = (0 · ((𝑤 − 𝑧)𝐼𝑧)))
262	104	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝐼:(ℝ × ℝ)⟶ℝ)
263	260, 236	eqeltrdi 2921	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑤 ∈ ℝ)
264	62	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → 𝑧 ∈ ℝ)
265	263, 264	resubcld 11062	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 − 𝑧) ∈ ℝ)
266	262, 265, 264	fovrnd 7314	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℝ)
267	266	recnd 10663	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → ((𝑤 − 𝑧)𝐼𝑧) ∈ ℂ)
268	267	mul02d 10832	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (0 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
269	261, 268	eqtrd 2856	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ {0}) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
270	258, 269	sylan2 594	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ran 𝐺) ∧ 𝑤 ∈ (ran 𝑃 ∖ (ran 𝑃 ∖ {0}))) → (𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = 0)
271	253, 254, 270, 127	fsumss 15076	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)) = Σ𝑤 ∈ ran 𝑃(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
272	167, 252, 271	3eqtr4d 2866	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
273	272	sumeq2dv 15054	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑧 ∈ ran 𝐺Σ𝑤 ∈ (ran 𝑃 ∖ {0})(𝑤 · ((𝑤 − 𝑧)𝐼𝑧)))
274	195	anasss 469	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹)) → ((𝑦 + 𝑧) · (𝑦𝐼𝑧)) ∈ ℂ)
275	7, 5, 274	fsumcom 15124	. 2 ⊢ (𝜑 → Σ𝑧 ∈ ran 𝐺Σ𝑦 ∈ ran 𝐹((𝑦 + 𝑧) · (𝑦𝐼𝑧)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
276	123, 273, 275	3eqtr2d 2862	1 ⊢ (𝜑 → (∫₁‘(𝐹 ∘_f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 {cab 2799 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 Vcvv 3495 ∖ cdif 3933 ∩ cin 3935 ⊆ wss 3936 ∅c0 4291 ifcif 4467 {csn 4561 ⟨cop 4567 ∪ ciun 4912 class class class wbr 5059 ↦ cmpt 5139 × cxp 5548 ^◡ccnv 5549 dom cdm 5550 ran crn 5551 ↾ cres 5552 “ cima 5553 Fun wfun 6344 Fn wfn 6345 ⟶wf 6346 –1-1→wf1 6347 –onto→wfo 6348 –1-1-onto→wf1o 6349 ‘cfv 6350 (class class class)co 7150 ∈ cmpo 7152 ∘_f cof 7401 Fincfn 8503 ℂcc 10529 ℝcr 10530 0cc0 10531 + caddc 10534 · cmul 10536 − cmin 10864 Σcsu 15036 vol*covol 24057 volcvol 24058 ∫₁citg1 24210

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609 ax-addf 10610

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-int 4870 df-iun 4914 df-disj 5025 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-se 5510 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-isom 6359 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-of 7403 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-2o 8097 df-oadd 8100 df-er 8283 df-map 8402 df-pm 8403 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-sup 8900 df-inf 8901 df-oi 8968 df-dju 9324 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-q 12343 df-rp 12384 df-xadd 12502 df-ioo 12736 df-ico 12738 df-icc 12739 df-fz 12887 df-fzo 13028 df-fl 13156 df-seq 13364 df-exp 13424 df-hash 13685 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-clim 14839 df-sum 15037 df-xmet 20532 df-met 20533 df-ovol 24059 df-vol 24060 df-mbf 24214 df-itg1 24215

This theorem is referenced by: itg1addlem5 24295

W3C validator