Metamath Proof Explorer

Theorem itg1addlem4

Description: Lemma for itg1add . (Contributed by Mario Carneiro, 28-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 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 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 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) )