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 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 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 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 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 ‘ 𝐺 ) ) )