Metamath Proof Explorer


Theorem itg1addlem4OLD

Description: Obsolete version of itg1addlem4 . (Contributed by Mario Carneiro, 28-Jun-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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