Theorem itg1addlem4OLD

Description: Obsolete version of itg1addlem4 as of 6-Oct-2024. (Contributed by Mario Carneiro, 28-Jun-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	i1fadd.1	⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
	i1fadd.2	⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
	itg1add.3	⊢ 𝐼 = ( 𝑖 ∈ ℝ , 𝑗 ∈ ℝ ↦ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) )
	itg1add.4	⊢ 𝑃 = ( + ↾ ( ran 𝐹 × ran 𝐺 ) )
Assertion	itg1addlem4OLD	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2		i1fadd.2	⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
3		itg1add.3	⊢ 𝐼 = ( 𝑖 ∈ ℝ , 𝑗 ∈ ℝ ↦ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) )
4		itg1add.4	⊢ 𝑃 = ( + ↾ ( ran 𝐹 × ran 𝐺 ) )
5	1 2	i1fadd	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ dom ∫1 )
6		i1frn	⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
7	1 6	syl	⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
8		i1frn	⊢ ( 𝐺 ∈ dom ∫1 → ran 𝐺 ∈ Fin )
9	2 8	syl	⊢ ( 𝜑 → ran 𝐺 ∈ Fin )
10		xpfi	⊢ ( ( ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin ) → ( ran 𝐹 × ran 𝐺 ) ∈ Fin )
11	7 9 10	syl2anc	⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ∈ Fin )
12		ax-addf	⊢ + : ( ℂ × ℂ ) ⟶ ℂ
13		ffn	⊢ ( + : ( ℂ × ℂ ) ⟶ ℂ → + Fn ( ℂ × ℂ ) )
14	12 13	ax-mp	⊢ + Fn ( ℂ × ℂ )
15		i1ff	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
16	1 15	syl	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
17	16	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
18		ax-resscn	⊢ ℝ ⊆ ℂ
19	17 18	sstrdi	⊢ ( 𝜑 → ran 𝐹 ⊆ ℂ )
20		i1ff	⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
21	2 20	syl	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
22	21	frnd	⊢ ( 𝜑 → ran 𝐺 ⊆ ℝ )
23	22 18	sstrdi	⊢ ( 𝜑 → ran 𝐺 ⊆ ℂ )
24		xpss12	⊢ ( ( ran 𝐹 ⊆ ℂ ∧ ran 𝐺 ⊆ ℂ ) → ( ran 𝐹 × ran 𝐺 ) ⊆ ( ℂ × ℂ ) )
25	19 23 24	syl2anc	⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ⊆ ( ℂ × ℂ ) )
26		fnssres	⊢ ( ( + Fn ( ℂ × ℂ ) ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ ( ℂ × ℂ ) ) → ( + ↾ ( ran 𝐹 × ran 𝐺 ) ) Fn ( ran 𝐹 × ran 𝐺 ) )
27	14 25 26	sylancr	⊢ ( 𝜑 → ( + ↾ ( ran 𝐹 × ran 𝐺 ) ) Fn ( ran 𝐹 × ran 𝐺 ) )
28	4	fneq1i	⊢ ( 𝑃 Fn ( ran 𝐹 × ran 𝐺 ) ↔ ( + ↾ ( ran 𝐹 × ran 𝐺 ) ) Fn ( ran 𝐹 × ran 𝐺 ) )
29	27 28	sylibr	⊢ ( 𝜑 → 𝑃 Fn ( ran 𝐹 × ran 𝐺 ) )
30		dffn4	⊢ ( 𝑃 Fn ( ran 𝐹 × ran 𝐺 ) ↔ 𝑃 : ( ran 𝐹 × ran 𝐺 ) –onto→ ran 𝑃 )
31	29 30	sylib	⊢ ( 𝜑 → 𝑃 : ( ran 𝐹 × ran 𝐺 ) –onto→ ran 𝑃 )
32		fofi	⊢ ( ( ( ran 𝐹 × ran 𝐺 ) ∈ Fin ∧ 𝑃 : ( ran 𝐹 × ran 𝐺 ) –onto→ ran 𝑃 ) → ran 𝑃 ∈ Fin )
33	11 31 32	syl2anc	⊢ ( 𝜑 → ran 𝑃 ∈ Fin )
34		difss	⊢ ( ran 𝑃 ∖ { 0 } ) ⊆ ran 𝑃
35		ssfi	⊢ ( ( ran 𝑃 ∈ Fin ∧ ( ran 𝑃 ∖ { 0 } ) ⊆ ran 𝑃 ) → ( ran 𝑃 ∖ { 0 } ) ∈ Fin )
36	33 34 35	sylancl	⊢ ( 𝜑 → ( ran 𝑃 ∖ { 0 } ) ∈ Fin )
37		ffun	⊢ ( + : ( ℂ × ℂ ) ⟶ ℂ → Fun + )
38	12 37	ax-mp	⊢ Fun +
39	12	fdmi	⊢ dom + = ( ℂ × ℂ )
40	25 39	sseqtrrdi	⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ⊆ dom + )
41		funfvima2	⊢ ( ( Fun + ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ dom + ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ran 𝐹 × ran 𝐺 ) → ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) )
42	38 40 41	sylancr	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ran 𝐹 × ran 𝐺 ) → ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) )
43		opelxpi	⊢ ( ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ran 𝐹 × ran 𝐺 ) )
44	42 43	impel	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) )
45		df-ov	⊢ ( 𝑥 + 𝑦 ) = ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ )
46	4	rneqi	⊢ ran 𝑃 = ran ( + ↾ ( ran 𝐹 × ran 𝐺 ) )
47		df-ima	⊢ ( + “ ( ran 𝐹 × ran 𝐺 ) ) = ran ( + ↾ ( ran 𝐹 × ran 𝐺 ) )
48	46 47	eqtr4i	⊢ ran 𝑃 = ( + “ ( ran 𝐹 × ran 𝐺 ) )
49	44 45 48	3eltr4g	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( 𝑥 + 𝑦 ) ∈ ran 𝑃 )
50	16	ffnd	⊢ ( 𝜑 → 𝐹 Fn ℝ )
51		dffn3	⊢ ( 𝐹 Fn ℝ ↔ 𝐹 : ℝ ⟶ ran 𝐹 )
52	50 51	sylib	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ran 𝐹 )
53	21	ffnd	⊢ ( 𝜑 → 𝐺 Fn ℝ )
54		dffn3	⊢ ( 𝐺 Fn ℝ ↔ 𝐺 : ℝ ⟶ ran 𝐺 )
55	53 54	sylib	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ran 𝐺 )
56		reex	⊢ ℝ ∈ V
57	56	a1i	⊢ ( 𝜑 → ℝ ∈ V )
58		inidm	⊢ ( ℝ ∩ ℝ ) = ℝ
59	49 52 55 57 57 58	off	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : ℝ ⟶ ran 𝑃 )
60	59	frnd	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ⊆ ran 𝑃 )
61	60	ssdifd	⊢ ( 𝜑 → ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ⊆ ( ran 𝑃 ∖ { 0 } ) )
62	17	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ )
63	22	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ )
64	62 63	anim12dan	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺 ) ) → ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) )
65		readdcl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 + 𝑧 ) ∈ ℝ )
66	64 65	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺 ) ) → ( 𝑦 + 𝑧 ) ∈ ℝ )
67	66	ralrimivva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐺 ( 𝑦 + 𝑧 ) ∈ ℝ )
68		funimassov	⊢ ( ( Fun + ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ dom + ) → ( ( + “ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ℝ ↔ ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐺 ( 𝑦 + 𝑧 ) ∈ ℝ ) )
69	38 40 68	sylancr	⊢ ( 𝜑 → ( ( + “ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ℝ ↔ ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐺 ( 𝑦 + 𝑧 ) ∈ ℝ ) )
70	67 69	mpbird	⊢ ( 𝜑 → ( + “ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ℝ )
71	48 70	eqsstrid	⊢ ( 𝜑 → ran 𝑃 ⊆ ℝ )
72	71	ssdifd	⊢ ( 𝜑 → ( ran 𝑃 ∖ { 0 } ) ⊆ ( ℝ ∖ { 0 } ) )
73		itg1val2	⊢ ( ( ( 𝐹 ∘f + 𝐺 ) ∈ dom ∫1 ∧ ( ( ran 𝑃 ∖ { 0 } ) ∈ Fin ∧ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ⊆ ( ran 𝑃 ∖ { 0 } ) ∧ ( ran 𝑃 ∖ { 0 } ) ⊆ ( ℝ ∖ { 0 } ) ) ) → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) )
74	5 36 61 72 73	syl13anc	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) )
75	21	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → 𝐺 : ℝ ⟶ ℝ )
76	9	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ran 𝐺 ∈ Fin )
77		inss2	⊢ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } )
78	77	a1i	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } ) )
79		i1fima	⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∈ dom vol )
80	1 79	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∈ dom vol )
81		i1fima	⊢ ( 𝐺 ∈ dom ∫1 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
82	2 81	syl	⊢ ( 𝜑 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
83		inmbl	⊢ ( ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∈ dom vol ∧ ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) → ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
84	80 82 83	syl2anc	⊢ ( 𝜑 → ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
85	84	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
86	34 71	sstrid	⊢ ( 𝜑 → ( ran 𝑃 ∖ { 0 } ) ⊆ ℝ )
87	86	sselda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → 𝑤 ∈ ℝ )
88	87	adantr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑤 ∈ ℝ )
89	63	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ )
90	88 89	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑤 − 𝑧 ) ∈ ℝ )
91	88	recnd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑤 ∈ ℂ )
92	89	recnd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℂ )
93	91 92	npcand	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) = 𝑤 )
94		eldifsni	⊢ ( 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) → 𝑤 ≠ 0 )
95	94	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑤 ≠ 0 )
96	93 95	eqnetrd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) ≠ 0 )
97		oveq12	⊢ ( ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) = ( 0 + 0 ) )
98		00id	⊢ ( 0 + 0 ) = 0
99	97 98	eqtrdi	⊢ ( ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) = 0 )
100	99	necon3ai	⊢ ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) ≠ 0 → ¬ ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) )
101	96 100	syl	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ¬ ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) )
102	1 2 3	itg1addlem3	⊢ ( ( ( ( 𝑤 − 𝑧 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ¬ ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
103	90 89 101 102	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
104	1 2 3	itg1addlem2	⊢ ( 𝜑 → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
105	104	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
106	105 90 89	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ∈ ℝ )
107	103 106	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
108	75 76 78 85 107	itg1addlem1	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( vol ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑧 ∈ ran 𝐺 ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
109	87	recnd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → 𝑤 ∈ ℂ )
110	1 2	i1faddlem	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) )
111	109 110	syldan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) )
112	111	fveq2d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) = ( vol ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
113	103	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → Σ 𝑧 ∈ ran 𝐺 ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) = Σ 𝑧 ∈ ran 𝐺 ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
114	108 112 113	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) = Σ 𝑧 ∈ ran 𝐺 ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) )
115	114	oveq2d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) = ( 𝑤 · Σ 𝑧 ∈ ran 𝐺 ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
116	106	recnd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ∈ ℂ )
117	76 109 116	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( 𝑤 · Σ 𝑧 ∈ ran 𝐺 ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
118	115 117	eqtrd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
119	118	sumeq2dv	⊢ ( 𝜑 → Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) = Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) Σ 𝑧 ∈ ran 𝐺 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
120	91 116	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ∈ ℂ )
121	120	anasss	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ∈ ℂ )
122	36 9 121	fsumcom	⊢ ( 𝜑 → Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) Σ 𝑧 ∈ ran 𝐺 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
123	74 119 122	3eqtrd	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑧 ∈ ran 𝐺 Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
124		oveq1	⊢ ( 𝑦 = ( 𝑤 − 𝑧 ) → ( 𝑦 + 𝑧 ) = ( ( 𝑤 − 𝑧 ) + 𝑧 ) )
125		oveq1	⊢ ( 𝑦 = ( 𝑤 − 𝑧 ) → ( 𝑦 𝐼 𝑧 ) = ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) )
126	124 125	oveq12d	⊢ ( 𝑦 = ( 𝑤 − 𝑧 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
127	33	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝑃 ∈ Fin )
128	71	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝑃 ⊆ ℝ )
129	128	sselda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑣 ∈ ran 𝑃 ) → 𝑣 ∈ ℝ )
130	63	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑣 ∈ ran 𝑃 ) → 𝑧 ∈ ℝ )
131	129 130	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑣 ∈ ran 𝑃 ) → ( 𝑣 − 𝑧 ) ∈ ℝ )
132	131	ex	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑣 ∈ ran 𝑃 → ( 𝑣 − 𝑧 ) ∈ ℝ ) )
133	129	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑣 ∈ ran 𝑃 ) → 𝑣 ∈ ℂ )
134	133	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → 𝑣 ∈ ℂ )
135	71	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑃 ) → 𝑦 ∈ ℝ )
136	135	ad2ant2rl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → 𝑦 ∈ ℝ )
137	136	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → 𝑦 ∈ ℂ )
138	63	recnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℂ )
139	138	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → 𝑧 ∈ ℂ )
140	134 137 139	subcan2ad	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → ( ( 𝑣 − 𝑧 ) = ( 𝑦 − 𝑧 ) ↔ 𝑣 = 𝑦 ) )
141	140	ex	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) → ( ( 𝑣 − 𝑧 ) = ( 𝑦 − 𝑧 ) ↔ 𝑣 = 𝑦 ) ) )
142	132 141	dom2lem	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1→ ℝ )
143		f1f1orn	⊢ ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1→ ℝ → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1-onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) )
144	142 143	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1-onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) )
145		oveq1	⊢ ( 𝑣 = 𝑤 → ( 𝑣 − 𝑧 ) = ( 𝑤 − 𝑧 ) )
146		eqid	⊢ ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) = ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) )
147		ovex	⊢ ( 𝑤 − 𝑧 ) ∈ V
148	145 146 147	fvmpt	⊢ ( 𝑤 ∈ ran 𝑃 → ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ‘ 𝑤 ) = ( 𝑤 − 𝑧 ) )
149	148	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ‘ 𝑤 ) = ( 𝑤 − 𝑧 ) )
150		f1f	⊢ ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1→ ℝ → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 ⟶ ℝ )
151		frn	⊢ ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 ⟶ ℝ → ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ⊆ ℝ )
152	142 150 151	3syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ⊆ ℝ )
153	152	sselda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → 𝑦 ∈ ℝ )
154	63	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → 𝑧 ∈ ℝ )
155	153 154	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ( 𝑦 + 𝑧 ) ∈ ℝ )
156	104	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
157	156 153 154	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ )
158	155 157	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℝ )
159	158	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
160	126 127 144 149 159	fsumf1o	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ran 𝑃 ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
161	128	sselda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → 𝑤 ∈ ℝ )
162	161	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → 𝑤 ∈ ℂ )
163	138	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → 𝑧 ∈ ℂ )
164	162 163	npcand	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) = 𝑤 )
165	164	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
166	165	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑤 ∈ ran 𝑃 ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ran 𝑃 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
167	160 166	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ran 𝑃 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
168	40	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ran 𝐹 × ran 𝐺 ) ⊆ dom + )
169		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ran 𝐹 )
170		simplr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ran 𝐺 )
171	169 170	opelxpd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ran 𝐹 × ran 𝐺 ) )
172		funfvima2	⊢ ( ( Fun + ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ dom + ) → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ran 𝐹 × ran 𝐺 ) → ( + ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) )
173	38 172	mpan	⊢ ( ( ran 𝐹 × ran 𝐺 ) ⊆ dom + → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ran 𝐹 × ran 𝐺 ) → ( + ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) )
174	168 171 173	sylc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( + ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) )
175		df-ov	⊢ ( 𝑦 + 𝑧 ) = ( + ‘ ⟨ 𝑦 , 𝑧 ⟩ )
176	174 175 48	3eltr4g	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 + 𝑧 ) ∈ ran 𝑃 )
177	62	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ )
178	177	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℂ )
179	138	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℂ )
180	178 179	pncand	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( 𝑦 + 𝑧 ) − 𝑧 ) = 𝑦 )
181	180	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 = ( ( 𝑦 + 𝑧 ) − 𝑧 ) )
182		oveq1	⊢ ( 𝑣 = ( 𝑦 + 𝑧 ) → ( 𝑣 − 𝑧 ) = ( ( 𝑦 + 𝑧 ) − 𝑧 ) )
183	182	rspceeqv	⊢ ( ( ( 𝑦 + 𝑧 ) ∈ ran 𝑃 ∧ 𝑦 = ( ( 𝑦 + 𝑧 ) − 𝑧 ) ) → ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) )
184	176 181 183	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) )
185	184	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ∀ 𝑦 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) )
186		ssabral	⊢ ( ran 𝐹 ⊆ { 𝑦 ∣ ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) } ↔ ∀ 𝑦 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) )
187	185 186	sylibr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝐹 ⊆ { 𝑦 ∣ ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) } )
188	146	rnmpt	⊢ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) = { 𝑦 ∣ ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) }
189	187 188	sseqtrrdi	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝐹 ⊆ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) )
190	63	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℝ )
191	177 190	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 + 𝑧 ) ∈ ℝ )
192	104	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
193	192 177 190	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ )
194	191 193	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℝ )
195	194	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
196	152	ssdifd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∖ ran 𝐹 ) ⊆ ( ℝ ∖ ran 𝐹 ) )
197	196	sselda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ( ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∖ ran 𝐹 ) ) → 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) )
198		eldifi	⊢ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) → 𝑦 ∈ ℝ )
199	198	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → 𝑦 ∈ ℝ )
200	63	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → 𝑧 ∈ ℝ )
201		simprr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) )
202	1 2 3	itg1addlem3	⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
203	199 200 201 202	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
204		inss1	⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑦 } )
205		eldifn	⊢ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) → ¬ 𝑦 ∈ ran 𝐹 )
206	205	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ¬ 𝑦 ∈ ran 𝐹 )
207		vex	⊢ 𝑣 ∈ V
208	207	eliniseg	⊢ ( 𝑦 ∈ V → ( 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↔ 𝑣 𝐹 𝑦 ) )
209	208	elv	⊢ ( 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↔ 𝑣 𝐹 𝑦 )
210		vex	⊢ 𝑦 ∈ V
211	207 210	brelrn	⊢ ( 𝑣 𝐹 𝑦 → 𝑦 ∈ ran 𝐹 )
212	209 211	sylbi	⊢ ( 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) → 𝑦 ∈ ran 𝐹 )
213	206 212	nsyl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ¬ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) )
214	213	pm2.21d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) → 𝑣 ∈ ∅ ) )
215	214	ssrdv	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ∅ )
216	204 215	sstrid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ∅ )
217		ss0	⊢ ( ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ∅ → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ∅ )
218	216 217	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ∅ )
219	218	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = ( vol ‘ ∅ ) )
220		0mbl	⊢ ∅ ∈ dom vol
221		mblvol	⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) )
222	220 221	ax-mp	⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ )
223		ovol0	⊢ ( vol* ‘ ∅ ) = 0
224	222 223	eqtri	⊢ ( vol ‘ ∅ ) = 0
225	219 224	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = 0 )
226	203 225	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑦 𝐼 𝑧 ) = 0 )
227	226	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( ( 𝑦 + 𝑧 ) · 0 ) )
228	199 200	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑦 + 𝑧 ) ∈ ℝ )
229	228	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑦 + 𝑧 ) ∈ ℂ )
230	229	mul01d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( 𝑦 + 𝑧 ) · 0 ) = 0 )
231	227 230	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 )
232	231	expr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ) → ( ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 ) )
233		oveq12	⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( 𝑦 + 𝑧 ) = ( 0 + 0 ) )
234	233 98	eqtrdi	⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( 𝑦 + 𝑧 ) = 0 )
235		oveq12	⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( 𝑦 𝐼 𝑧 ) = ( 0 𝐼 0 ) )
236		0re	⊢ 0 ∈ ℝ
237		iftrue	⊢ ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) = 0 )
238		c0ex	⊢ 0 ∈ V
239	237 3 238	ovmpoa	⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 0 𝐼 0 ) = 0 )
240	236 236 239	mp2an	⊢ ( 0 𝐼 0 ) = 0
241	235 240	eqtrdi	⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( 𝑦 𝐼 𝑧 ) = 0 )
242	234 241	oveq12d	⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( 0 · 0 ) )
243		0cn	⊢ 0 ∈ ℂ
244	243	mul01i	⊢ ( 0 · 0 ) = 0
245	242 244	eqtrdi	⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 )
246	232 245	pm2.61d2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 )
247	197 246	syldan	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ( ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∖ ran 𝐹 ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 )
248		f1ofo	⊢ ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1-onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) )
249	144 248	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) )
250		fofi	⊢ ( ( ran 𝑃 ∈ Fin ∧ ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∈ Fin )
251	127 249 250	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∈ Fin )
252	189 195 247 251	fsumss	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑦 ∈ ran 𝐹 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) )
253	34	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( ran 𝑃 ∖ { 0 } ) ⊆ ran 𝑃 )
254	120	an32s	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ∈ ℂ )
255		dfin4	⊢ ( ran 𝑃 ∩ { 0 } ) = ( ran 𝑃 ∖ ( ran 𝑃 ∖ { 0 } ) )
256		inss2	⊢ ( ran 𝑃 ∩ { 0 } ) ⊆ { 0 }
257	255 256	eqsstrri	⊢ ( ran 𝑃 ∖ ( ran 𝑃 ∖ { 0 } ) ) ⊆ { 0 }
258	257	sseli	⊢ ( 𝑤 ∈ ( ran 𝑃 ∖ ( ran 𝑃 ∖ { 0 } ) ) → 𝑤 ∈ { 0 } )
259		elsni	⊢ ( 𝑤 ∈ { 0 } → 𝑤 = 0 )
260	259	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → 𝑤 = 0 )
261	260	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = ( 0 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
262	104	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
263	260 236	eqeltrdi	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → 𝑤 ∈ ℝ )
264	63	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → 𝑧 ∈ ℝ )
265	263 264	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( 𝑤 − 𝑧 ) ∈ ℝ )
266	262 265 264	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ∈ ℝ )
267	266	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ∈ ℂ )
268	267	mul02d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( 0 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = 0 )
269	261 268	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = 0 )
270	258 269	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ( ran 𝑃 ∖ ( ran 𝑃 ∖ { 0 } ) ) ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = 0 )
271	253 254 270 127	fsumss	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ran 𝑃 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
272	167 252 271	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑦 ∈ ran 𝐹 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
273	272	sumeq2dv	⊢ ( 𝜑 → Σ 𝑧 ∈ ran 𝐺 Σ 𝑦 ∈ ran 𝐹 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) )
274	195	anasss	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹 ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
275	9 7 274	fsumcom	⊢ ( 𝜑 → Σ 𝑧 ∈ ran 𝐺 Σ 𝑦 ∈ ran 𝐹 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) )
276	123 273 275	3eqtr2d	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) )