Metamath Proof Explorer

Theorem i1fmul

Description: The pointwise product of two simple functions is a simple function. (Contributed by Mario Carneiro, 5-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 i1fadd.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2 i1fadd.2 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
3 remulcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
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 ax-resscn ⊢ ℝ ⊆ ℂ
48 46 47 sstrdi ⊢ ( 𝜑 → ran ( 𝐹 ∘f · 𝐺 ) ⊆ ℂ )
49 48 ssdifd ⊢ ( 𝜑 → ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } ) )
50 49 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → 𝑦 ∈ ( ℂ ∖ { 0 } ) )
51 1 2 i1fmullem ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) = ∪ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) )
52 50 51 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) = ∪ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) )
53 difss ⊢ ( ran 𝐺 ∖ { 0 } ) ⊆ ran 𝐺
54 ssfi ⊢ ( ( ran 𝐺 ∈ Fin ∧ ( ran 𝐺 ∖ { 0 } ) ⊆ ran 𝐺 ) → ( ran 𝐺 ∖ { 0 } ) ∈ Fin )
55 16 53 54 sylancl ⊢ ( 𝜑 → ( ran 𝐺 ∖ { 0 } ) ∈ Fin )
56 i1fima ⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∈ dom vol )
57 1 56 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∈ dom vol )
58 i1fima ⊢ ( 𝐺 ∈ dom ∫1 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
59 2 58 syl ⊢ ( 𝜑 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
60 inmbl ⊢ ( ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∈ dom vol ∧ ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) → ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
61 57 59 60 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
62 61 ralrimivw ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
63 finiunmbl ⊢ ( ( ( ran 𝐺 ∖ { 0 } ) ∈ Fin ∧ ∀ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol ) → ∪ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
64 55 62 63 syl2anc ⊢ ( 𝜑 → ∪ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ∪ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol )
66 52 65 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ∈ dom vol )
67 mblvol ⊢ ( ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ∈ dom vol → ( vol ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) = ( vol* ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) )
68 66 67 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) = ( vol* ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) )
69 mblss ⊢ ( ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ∈ dom vol → ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ⊆ ℝ )
70 66 69 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ⊆ ℝ )
71 55 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( ran 𝐺 ∖ { 0 } ) ∈ Fin )
72 inss2 ⊢ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } )
73 72 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } ) )
74 59 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol )
75 mblss ⊢ ( ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol → ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ℝ )
76 74 75 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ℝ )
77 mblvol ⊢ ( ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( vol* ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) )
78 74 77 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( vol* ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) )
79 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → 𝐺 ∈ dom ∫1 )
80 i1fima2sn ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ ℝ )
81 79 80 sylan ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ ℝ )
82 78 81 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol* ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ ℝ )
83 ovolsscl ⊢ ( ( ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } ) ∧ ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ ℝ ) → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
84 73 76 82 83 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
85 71 84 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ )
86 52 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( vol* ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) = ( vol* ‘ ∪ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
87 mblss ⊢ ( ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol → ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ )
88 61 87 syl ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ )
89 88 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ )
90 89 84 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) )
91 90 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ∀ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) )
92 ovolfiniun ⊢ ( ( ( ran 𝐺 ∖ { 0 } ) ∈ Fin ∧ ∀ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ℝ ∧ ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ≤ Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
93 71 91 92 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( vol* ‘ ∪ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ≤ Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
94 86 93 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( vol* ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) ≤ Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) )
95 ovollecl ⊢ ( ( ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ⊆ ℝ ∧ Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ∧ ( vol* ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) ≤ Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( vol* ‘ ( ( ◡ 𝐹 “ { ( 𝑦 / 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) → ( vol* ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) ∈ ℝ )
96 70 85 94 95 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( vol* ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) ∈ ℝ )
97 68 96 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran ( 𝐹 ∘f · 𝐺 ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝑦 } ) ) ∈ ℝ )
98 12 45 66 97 i1fd ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ dom ∫1 )