Metamath Proof Explorer


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 fovrnd ( ( ( 𝜑𝑦 ∈ 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 fovrnd ( ( ( 𝜑𝑦 ∈ ( 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 syl5eq ( ( 𝜑𝑦 ∈ ( 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 fovrnd ( ( ( 𝜑𝑦 ∈ { 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 fovrnd ( ( ( 𝜑𝑧 ∈ ( 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 syl5eq ( ( 𝜑𝑧 ∈ ( 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 fovrnd ( ( ( 𝜑𝑧 ∈ { 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 fovrnd ( ( ( 𝜑𝑧 ∈ 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𝐺 ) ) )