Theorem itg1addlem4

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

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