Theorem itg1addlem5

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

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

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		i1frn	⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
6	1 5	syl	⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
7		i1frn	⊢ ( 𝐺 ∈ dom ∫1 → ran 𝐺 ∈ Fin )
8	2 7	syl	⊢ ( 𝜑 → ran 𝐺 ∈ Fin )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → ran 𝐺 ∈ Fin )
10		i1ff	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
11	1 10	syl	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
12	11	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
13	12	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ )
14	13	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℝ )
15	14	recnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℂ )
16	1 2 3	itg1addlem2	⊢ ( 𝜑 → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
17	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
18		i1ff	⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
19	2 18	syl	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
20	19	frnd	⊢ ( 𝜑 → ran 𝐺 ⊆ ℝ )
21	20	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ )
22	21	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ )
23	17 14 22	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ )
24	23	recnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ )
25	15 24	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
26	9 25	fsumcl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
27	22	recnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℂ )
28	27 24	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
29	9 28	fsumcl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
30	6 26 29	fsumadd	⊢ ( 𝜑 → Σ 𝑦 ∈ ran 𝐹 ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) = ( Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) )
31	1 2 3 4	itg1addlem4	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) )
32	15 27 24	adddird	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) )
33	32	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) )
34	9 25 28	fsumadd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) = ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) )
35	33 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) )
36	35	sumeq2dv	⊢ ( 𝜑 → Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) )
37	31 36	eqtrd	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑦 ∈ ran 𝐹 ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) )
38		itg1val	⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) )
39	1 38	syl	⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) = Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) )
40	19	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐺 : ℝ ⟶ ℝ )
41	8	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ran 𝐺 ∈ Fin )
42		inss2	⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } )
43	42	a1i	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } ) )
44		i1fima	⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
45	1 44	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
46	45	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
47		i1fima	⊢ ( 𝐺 ∈ dom ∫1 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
48	2 47	syl	⊢ ( 𝜑 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
49	48	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
50		inmbl	⊢ ( ( ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ∧ ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
51	46 49 50	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
52	12	ssdifssd	⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ℝ )
53	52	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑦 ∈ ℝ )
54	53	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℝ )
55	20	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ran 𝐺 ⊆ ℝ )
56	55	sselda	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ )
57		eldifsni	⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑦 ≠ 0 )
58	57	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ≠ 0 )
59		simpl	⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → 𝑦 = 0 )
60	59	necon3ai	⊢ ( 𝑦 ≠ 0 → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) )
61	58 60	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) )
62	1 2 3	itg1addlem3	⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
63	54 56 61 62	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
64	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
65	64 54 56	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ )
66	63 65	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
67	40 41 43 51 66	itg1addlem1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑧 ∈ ran 𝐺 ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
68		iunin2	⊢ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) )
69	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐹 ∈ dom ∫1 )
70	69 44	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
71		mblss	⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ )
72	70 71	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ )
73		iunid	⊢ ∪ 𝑧 ∈ ran 𝐺 { 𝑧 } = ran 𝐺
74	73	imaeq2i	⊢ ( ◡ 𝐺 “ ∪ 𝑧 ∈ ran 𝐺 { 𝑧 } ) = ( ◡ 𝐺 “ ran 𝐺 )
75		imaiun	⊢ ( ◡ 𝐺 “ ∪ 𝑧 ∈ ran 𝐺 { 𝑧 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } )
76		cnvimarndm	⊢ ( ◡ 𝐺 “ ran 𝐺 ) = dom 𝐺
77	74 75 76	3eqtr3i	⊢ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) = dom 𝐺
78	40	fdmd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → dom 𝐺 = ℝ )
79	77 78	eqtrid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) = ℝ )
80	72 79	sseqtrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) )
81		df-ss	⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) ↔ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ◡ 𝐹 “ { 𝑦 } ) )
82	80 81	sylib	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ◡ 𝐹 “ { 𝑦 } ) )
83	68 82	eqtr2id	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) )
84	83	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) = ( vol ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
85	63	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 𝐼 𝑧 ) = Σ 𝑧 ∈ ran 𝐺 ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
86	67 84 85	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑦 𝐼 𝑧 ) )
87	86	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) = ( 𝑦 · Σ 𝑧 ∈ ran 𝐺 ( 𝑦 𝐼 𝑧 ) ) )
88	53	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
89	65	recnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ )
90	41 88 89	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑦 · Σ 𝑧 ∈ ran 𝐺 ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) )
91	87 90	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) )
92	91	sumeq2dv	⊢ ( 𝜑 → Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) = Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) )
93		difssd	⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 )
94	54	recnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℂ )
95	94 89	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
96	41 95	fsumcl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
97		dfin4	⊢ ( ran 𝐹 ∩ { 0 } ) = ( ran 𝐹 ∖ ( ran 𝐹 ∖ { 0 } ) )
98		inss2	⊢ ( ran 𝐹 ∩ { 0 } ) ⊆ { 0 }
99	97 98	eqsstrri	⊢ ( ran 𝐹 ∖ ( ran 𝐹 ∖ { 0 } ) ) ⊆ { 0 }
100	99	sseli	⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ ( ran 𝐹 ∖ { 0 } ) ) → 𝑦 ∈ { 0 } )
101		elsni	⊢ ( 𝑦 ∈ { 0 } → 𝑦 = 0 )
102	101	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 = 0 )
103	102	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = ( 0 · ( 𝑦 𝐼 𝑧 ) ) )
104	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
105		0re	⊢ 0 ∈ ℝ
106	102 105	eqeltrdi	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℝ )
107	21	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ )
108	104 106 107	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ )
109	108	recnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ )
110	109	mul02d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 0 · ( 𝑦 𝐼 𝑧 ) ) = 0 )
111	103 110	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = 0 )
112	111	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 0 )
113	8	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → ran 𝐺 ∈ Fin )
114	113	olcd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → ( ran 𝐺 ⊆ ( ℤ≥ ‘ 0 ) ∨ ran 𝐺 ∈ Fin ) )
115		sumz	⊢ ( ( ran 𝐺 ⊆ ( ℤ≥ ‘ 0 ) ∨ ran 𝐺 ∈ Fin ) → Σ 𝑧 ∈ ran 𝐺 0 = 0 )
116	114 115	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → Σ 𝑧 ∈ ran 𝐺 0 = 0 )
117	112 116	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = 0 )
118	100 117	sylan2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = 0 )
119	93 96 118 6	fsumss	⊢ ( 𝜑 → Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) )
120	39 92 119	3eqtrd	⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) )
121		itg1val	⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) = Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
122	2 121	syl	⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) = Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
123	11	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝐹 : ℝ ⟶ ℝ )
124	6	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ran 𝐹 ∈ Fin )
125		inss1	⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑦 } )
126	125	a1i	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑦 } ) )
127	45	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
128	48	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
129	127 128 50	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
130	12	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ran 𝐹 ⊆ ℝ )
131	130	sselda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ )
132	20	ssdifssd	⊢ ( 𝜑 → ( ran 𝐺 ∖ { 0 } ) ⊆ ℝ )
133	132	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝑧 ∈ ℝ )
134	133	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℝ )
135		eldifsni	⊢ ( 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) → 𝑧 ≠ 0 )
136	135	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ≠ 0 )
137		simpr	⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → 𝑧 = 0 )
138	137	necon3ai	⊢ ( 𝑧 ≠ 0 → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) )
139	136 138	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) )
140	131 134 139 62	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
141	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
142	141 131 134	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ )
143	140 142	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
144	123 124 126 129 143	itg1addlem1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑦 ∈ ran 𝐹 ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
145		incom	⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ( ◡ 𝐹 “ { 𝑦 } ) )
146	145	a1i	⊢ ( 𝑦 ∈ ran 𝐹 → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) )
147	146	iuneq2i	⊢ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ( ◡ 𝐹 “ { 𝑦 } ) )
148		iunin2	⊢ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) = ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) )
149	147 148	eqtri	⊢ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) )
150		cnvimass	⊢ ( ◡ 𝐺 “ { 𝑧 } ) ⊆ dom 𝐺
151	19	fdmd	⊢ ( 𝜑 → dom 𝐺 = ℝ )
152	151	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → dom 𝐺 = ℝ )
153	150 152	sseqtrid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ℝ )
154		iunid	⊢ ∪ 𝑦 ∈ ran 𝐹 { 𝑦 } = ran 𝐹
155	154	imaeq2i	⊢ ( ◡ 𝐹 “ ∪ 𝑦 ∈ ran 𝐹 { 𝑦 } ) = ( ◡ 𝐹 “ ran 𝐹 )
156		imaiun	⊢ ( ◡ 𝐹 “ ∪ 𝑦 ∈ ran 𝐹 { 𝑦 } ) = ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } )
157		cnvimarndm	⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
158	155 156 157	3eqtr3i	⊢ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) = dom 𝐹
159	11	fdmd	⊢ ( 𝜑 → dom 𝐹 = ℝ )
160	159	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → dom 𝐹 = ℝ )
161	158 160	eqtrid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) = ℝ )
162	153 161	sseqtrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) )
163		df-ss	⊢ ( ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) ↔ ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) ) = ( ◡ 𝐺 “ { 𝑧 } ) )
164	162 163	sylib	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) ) = ( ◡ 𝐺 “ { 𝑧 } ) )
165	149 164	eqtr2id	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) = ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) )
166	165	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( vol ‘ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
167	140	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑦 𝐼 𝑧 ) = Σ 𝑦 ∈ ran 𝐹 ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
168	144 166 167	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) = Σ 𝑦 ∈ ran 𝐹 ( 𝑦 𝐼 𝑧 ) )
169	168	oveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = ( 𝑧 · Σ 𝑦 ∈ ran 𝐹 ( 𝑦 𝐼 𝑧 ) ) )
170	133	recnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝑧 ∈ ℂ )
171	142	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ )
172	124 170 171	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 · Σ 𝑦 ∈ ran 𝐹 ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) )
173	169 172	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) )
174	173	sumeq2dv	⊢ ( 𝜑 → Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) )
175		difssd	⊢ ( 𝜑 → ( ran 𝐺 ∖ { 0 } ) ⊆ ran 𝐺 )
176	170	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℂ )
177	176 171	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
178	124 177	fsumcl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
179		dfin4	⊢ ( ran 𝐺 ∩ { 0 } ) = ( ran 𝐺 ∖ ( ran 𝐺 ∖ { 0 } ) )
180		inss2	⊢ ( ran 𝐺 ∩ { 0 } ) ⊆ { 0 }
181	179 180	eqsstrri	⊢ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { 0 } ) ) ⊆ { 0 }
182	181	sseli	⊢ ( 𝑧 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { 0 } ) ) → 𝑧 ∈ { 0 } )
183		elsni	⊢ ( 𝑧 ∈ { 0 } → 𝑧 = 0 )
184	183	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 = 0 )
185	184	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = ( 0 · ( 𝑦 𝐼 𝑧 ) ) )
186	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
187	13	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ )
188	184 105	eqeltrdi	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℝ )
189	186 187 188	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ )
190	189	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ )
191	190	mul02d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 0 · ( 𝑦 𝐼 𝑧 ) ) = 0 )
192	185 191	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = 0 )
193	192	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 0 )
194	6	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → ran 𝐹 ∈ Fin )
195	194	olcd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → ( ran 𝐹 ⊆ ( ℤ≥ ‘ 0 ) ∨ ran 𝐹 ∈ Fin ) )
196		sumz	⊢ ( ( ran 𝐹 ⊆ ( ℤ≥ ‘ 0 ) ∨ ran 𝐹 ∈ Fin ) → Σ 𝑦 ∈ ran 𝐹 0 = 0 )
197	195 196	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → Σ 𝑦 ∈ ran 𝐹 0 = 0 )
198	193 197	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = 0 )
199	182 198	sylan2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { 0 } ) ) ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = 0 )
200	175 178 199 8	fsumss	⊢ ( 𝜑 → Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) )
201	21	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℝ )
202	201	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℂ )
203	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ )
204	12	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝐹 ⊆ ℝ )
205	204	sselda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ )
206	203 205 201	fovcdmd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ )
207	206	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ )
208	202 207	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
209	208	anasss	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹 ) ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ )
210	8 6 209	fsumcom	⊢ ( 𝜑 → Σ 𝑧 ∈ ran 𝐺 Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) )
211	200 210	eqtrd	⊢ ( 𝜑 → Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) )
212	122 174 211	3eqtrd	⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) )
213	120 212	oveq12d	⊢ ( 𝜑 → ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ 𝐺 ) ) = ( Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) )
214	30 37 213	3eqtr4d	⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ 𝐺 ) ) )