Metamath Proof Explorer


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 fovrnd ( ( ( 𝜑𝑤 ∈ ( 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 fovrnd ( ( ( 𝜑𝑧 ∈ 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 fovrnd ( ( ( 𝜑𝑧 ∈ 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 fovrnd ( ( ( 𝜑𝑧 ∈ 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 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) )