Metamath Proof Explorer

Theorem i1fadd

Description: The sum of two simple functions is a simple function. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses i1fadd.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
i1fadd.2 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
Assertion i1fadd ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ dom ∫1 )

Proof

Step Hyp Ref Expression
1 i1fadd.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2 i1fadd.2 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
3 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
4 3 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
5 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
6 1 5 syl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
7 i1ff ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
8 2 7 syl ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
9 reex ⊢ ℝ ∈ V
10 9 a1i ⊢ ( 𝜑 → ℝ ∈ V )
11 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
12 4 6 8 10 10 11 off ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : ℝ ⟶ ℝ )
13 i1frn ⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
14 1 13 syl ⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
15 i1frn ⊢ ( 𝐺 ∈ dom ∫1 → ran 𝐺 ∈ Fin )
16 2 15 syl ⊢ ( 𝜑 → ran 𝐺 ∈ Fin )
17 xpfi ⊢ ( ( ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin ) → ( ran 𝐹 × ran 𝐺 ) ∈ Fin )
18 14 16 17 syl2anc ⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ∈ Fin )
19 eqid ⊢ ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) = ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) )
20 ovex ⊢ ( 𝑢 + 𝑣 ) ∈ V
21 19 20 fnmpoi ⊢ ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) Fn ( ran 𝐹 × ran 𝐺 )
22 dffn4 ⊢ ( ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) Fn ( ran 𝐹 × ran 𝐺 ) ↔ ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) : ( ran 𝐹 × ran 𝐺 ) –onto→ ran ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) )
23 21 22 mpbi ⊢ ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) : ( ran 𝐹 × ran 𝐺 ) –onto→ ran ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) )
24 fofi ⊢ ( ( ( ran 𝐹 × ran 𝐺 ) ∈ Fin ∧ ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) : ( ran 𝐹 × ran 𝐺 ) –onto→ ran ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) ) → ran ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) ∈ Fin )
25 18 23 24 sylancl ⊢ ( 𝜑 → ran ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) ∈ Fin )
26 eqid ⊢ ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑦 )
27 rspceov ⊢ ( ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ∧ ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑦 ) ) → ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑣 ) )
28 26 27 mp3an3 ⊢ ( ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ) → ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑣 ) )
29 ovex ⊢ ( 𝑥 + 𝑦 ) ∈ V
30 eqeq1 ⊢ ( 𝑤 = ( 𝑥 + 𝑦 ) → ( 𝑤 = ( 𝑢 + 𝑣 ) ↔ ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑣 ) ) )
31 30 2rexbidv ⊢ ( 𝑤 = ( 𝑥 + 𝑦 ) → ( ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 𝑤 = ( 𝑢 + 𝑣 ) ↔ ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑣 ) ) )
32 29 31 elab ⊢ ( ( 𝑥 + 𝑦 ) ∈ { 𝑤 ∣ ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 𝑤 = ( 𝑢 + 𝑣 ) } ↔ ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 ( 𝑥 + 𝑦 ) = ( 𝑢 + 𝑣 ) )
33 28 32 sylibr ⊢ ( ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ) → ( 𝑥 + 𝑦 ) ∈ { 𝑤 ∣ ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 𝑤 = ( 𝑢 + 𝑣 ) } )
34 33 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( 𝑥 + 𝑦 ) ∈ { 𝑤 ∣ ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 𝑤 = ( 𝑢 + 𝑣 ) } )
35 6 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
36 dffn3 ⊢ ( 𝐹 Fn ℝ ↔ 𝐹 : ℝ ⟶ ran 𝐹 )
37 35 36 sylib ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ran 𝐹 )
38 8 ffnd ⊢ ( 𝜑 → 𝐺 Fn ℝ )
39 dffn3 ⊢ ( 𝐺 Fn ℝ ↔ 𝐺 : ℝ ⟶ ran 𝐺 )
40 38 39 sylib ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ran 𝐺 )
41 34 37 40 10 10 11 off ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : ℝ ⟶ { 𝑤 ∣ ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 𝑤 = ( 𝑢 + 𝑣 ) } )
42 41 frnd ⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ⊆ { 𝑤 ∣ ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 𝑤 = ( 𝑢 + 𝑣 ) } )
43 19 rnmpo ⊢ ran ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) = { 𝑤 ∣ ∃ 𝑢 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝐺 𝑤 = ( 𝑢 + 𝑣 ) }
44 42 43 sseqtrrdi ⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ⊆ ran ( 𝑢 ∈ ran 𝐹 , 𝑣 ∈ ran 𝐺 ↦ ( 𝑢 + 𝑣 ) ) )
45 25 44 ssfid ⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ∈ Fin )
46 12 frnd ⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ⊆ ℝ )
47 46 ssdifssd ⊢ ( 𝜑 → ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ⊆ ℝ )
48 47 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → 𝑦 ∈ ℝ )
49 48 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
50 1 2 i1faddlem ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) )
51 49 50 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) )
52 16 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ran 𝐺 ∈ Fin )
53 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐹 ∈ dom ∫1 )
54 i1fmbf ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ MblFn )
55 53 54 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐹 ∈ MblFn )
56 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐹 : ℝ ⟶ ℝ )
57 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝐹 ∘f + 𝐺 ) : ℝ ⟶ ℝ )
58 57 frnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ran ( 𝐹 ∘f + 𝐺 ) ⊆ ℝ )
59 eldifi ⊢ ( 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) → 𝑦 ∈ ran ( 𝐹 ∘f + 𝐺 ) )
60 59 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ran ( 𝐹 ∘f + 𝐺 ) )
61 58 60 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℝ )
62 8 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → 𝐺 : ℝ ⟶ ℝ )
63 62 frnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ran 𝐺 ⊆ ℝ )
64 63 sselda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ )
65 61 64 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 − 𝑧 ) ∈ ℝ )
66 mbfimasn ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : ℝ ⟶ ℝ ∧ ( 𝑦 − 𝑧 ) ∈ ℝ ) → ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∈ dom vol )
67 55 56 65 66 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∈ dom vol )
68 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐺 ∈ dom ∫1 )
69 i1fmbf ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 ∈ MblFn )
70 68 69 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐺 ∈ MblFn )
71 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐺 : ℝ ⟶ ℝ )
72 mbfimasn ⊢ ( ( 𝐺 ∈ MblFn ∧ 𝐺 : ℝ ⟶ ℝ ∧ 𝑧 ∈ ℝ ) → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
73 70 71 64 72 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
74 inmbl ⊢ ( ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∈ dom vol ∧ ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) → ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
75 67 73 74 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
76 75 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ∀ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
77 finiunmbl ⊢ ( ( ran 𝐺 ∈ Fin ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol ) → ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
78 52 76 77 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
79 51 78 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ∈ dom vol )
80 mblvol ⊢ ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ∈ dom vol → ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) = ( vol* ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) )
81 79 80 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) = ( vol* ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) )
82 mblss ⊢ ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ∈ dom vol → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ⊆ ℝ )
83 79 82 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ⊆ ℝ )
84 inss1 ⊢ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } )
85 67 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∈ dom vol )
86 mblss ⊢ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∈ dom vol → ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ⊆ ℝ )
87 85 86 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ⊆ ℝ )
88 mblvol ⊢ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ) )
89 85 88 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( vol ‘ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ) )
90 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → 𝑧 = 0 )
91 90 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( 𝑦 − 𝑧 ) = ( 𝑦 − 0 ) )
92 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → 𝑦 ∈ ℂ )
93 92 subid1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( 𝑦 − 0 ) = 𝑦 )
94 91 93 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( 𝑦 − 𝑧 ) = 𝑦 )
95 94 sneqd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → { ( 𝑦 − 𝑧 ) } = { 𝑦 } )
96 95 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) = ( ◡ 𝐹 “ { 𝑦 } ) )
97 96 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( vol ‘ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ) = ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) )
98 i1fima2sn ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
99 1 98 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
100 99 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
101 97 100 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( vol ‘ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ) ∈ ℝ )
102 89 101 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( vol* ‘ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ) ∈ ℝ )
103 ovolsscl ⊢ ( ( ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∧ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ) ∈ ℝ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
104 84 87 102 103 mp3an2i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 = 0 ) ) → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
105 104 expr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑧 = 0 → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) )
106 eldifsn ⊢ ( 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ↔ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 ≠ 0 ) )
107 inss2 ⊢ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } )
108 eldifi ⊢ ( 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) → 𝑧 ∈ ran 𝐺 )
109 mblss ⊢ ( ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol → ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ℝ )
110 73 109 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ℝ )
111 108 110 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ℝ )
112 i1fima ⊢ ( 𝐺 ∈ dom ∫1 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
113 2 112 syl ⊢ ( 𝜑 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
114 113 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
115 mblvol ⊢ ( ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( vol* ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) )
116 114 115 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( vol* ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) )
117 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → 𝐺 ∈ dom ∫1 )
118 i1fima2sn ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ ℝ )
119 117 118 sylan ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ ℝ )
120 116 119 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol* ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ ℝ )
121 ovolsscl ⊢ ( ( ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } ) ∧ ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ ℝ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
122 107 111 120 121 mp3an2i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
123 106 122 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑧 ≠ 0 ) ) → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
124 123 expr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑧 ≠ 0 → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) )
125 105 124 pm2.61dne ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
126 52 125 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → Σ 𝑧 ∈ ran 𝐺 ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
127 51 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( vol* ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) = ( vol* ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
128 107 110 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ )
129 128 125 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) )
130 129 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ∀ 𝑧 ∈ ran 𝐺 ( ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) )
131 ovolfiniun ⊢ ( ( ran 𝐺 ∈ Fin ∧ ∀ 𝑧 ∈ ran 𝐺 ( ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ≤ Σ 𝑧 ∈ ran 𝐺 ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
132 52 130 131 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( vol* ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ≤ Σ 𝑧 ∈ ran 𝐺 ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
133 127 132 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( vol* ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) ≤ Σ 𝑧 ∈ ran 𝐺 ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
134 ovollecl ⊢ ( ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ⊆ ℝ ∧ Σ 𝑧 ∈ ran 𝐺 ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ∧ ( vol* ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) ≤ Σ 𝑧 ∈ ran 𝐺 ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) → ( vol* ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) ∈ ℝ )
135 83 126 133 134 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( vol* ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) ∈ ℝ )
136 81 135 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑦 } ) ) ∈ ℝ )
137 12 45 79 136 i1fd ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ dom ∫1 )