This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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