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

Metamath Proof Explorer

Theorem bddmulibl

Description: A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Assertion bddmulibl ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 mbff ⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )
2 1 ad2antrr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
3 2 ffnd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐹 Fn dom 𝐹 )
4 iblmbf ⊢ ( 𝐺 ∈ 𝐿1 → 𝐺 ∈ MblFn )
5 4 ad2antlr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 ∈ MblFn )
6 mbff ⊢ ( 𝐺 ∈ MblFn → 𝐺 : dom 𝐺 ⟶ ℂ )
7 5 6 syl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 : dom 𝐺 ⟶ ℂ )
8 7 ffnd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 Fn dom 𝐺 )
9 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
10 9 ad2antrr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → dom 𝐹 ∈ dom vol )
11 mbfdm ⊢ ( 𝐺 ∈ MblFn → dom 𝐺 ∈ dom vol )
12 5 11 syl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → dom 𝐺 ∈ dom vol )
13 eqid ⊢ ( dom 𝐹 ∩ dom 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 )
14 eqidd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
15 eqidd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
16 3 8 10 12 13 14 15 offval ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝐹 ∘f · 𝐺 ) = ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
17 ovexd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ∈ V )
18 simpll ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐹 ∈ MblFn )
19 18 5 mbfmul ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ MblFn )
20 16 19 eqeltrrd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn )
21 absf ⊢ abs : ℂ ⟶ ℝ
22 21 a1i ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → abs : ℂ ⟶ ℝ )
23 20 17 mbfmptcl ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
24 22 23 cofmpt ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( abs ∘ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) )
25 23 fmpttd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℂ )
26 ax-resscn ⊢ ℝ ⊆ ℂ
27 ssid ⊢ ℂ ⊆ ℂ
28 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ ) )
29 26 27 28 mp2an ⊢ ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ )
30 abscncf ⊢ abs ∈ ( ℂ –cn→ ℝ )
31 29 30 sselii ⊢ abs ∈ ( ℂ –cn→ ℂ )
32 31 a1i ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → abs ∈ ( ℂ –cn→ ℂ ) )
33 cncombf ⊢ ( ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn ∧ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℂ ∧ abs ∈ ( ℂ –cn→ ℂ ) ) → ( abs ∘ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ MblFn )
34 20 25 32 33 syl3anc ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( abs ∘ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ MblFn )
35 24 34 eqeltrrd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ MblFn )
36 23 abscld ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ )
37 36 rexrd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ* )
38 23 absge0d ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
39 elxrge0 ⊢ ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) )
40 37 38 39 sylanbrc ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 0 [,] +∞ ) )
41 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
42 41 a1i ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ∈ ( 0 [,] +∞ ) )
43 40 42 ifclda ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
44 43 adantr ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
45 44 fmpttd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
46 reex ⊢ ℝ ∈ V
47 46 a1i ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ℝ ∈ V )
48 simprl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
49 48 ad2antrr ⊢ ( ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) ∧ 𝑧 ∈ ℝ ) → 𝑥 ∈ ℝ )
50 elinel2 ⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑧 ∈ dom 𝐺 )
51 ffvelcdm ⊢ ( ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ 𝑧 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
52 7 50 51 syl2an ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
53 52 abscld ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ )
54 52 absge0d ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) )
55 elrege0 ⊢ ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
56 53 54 55 sylanbrc ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( 0 [,) +∞ ) )
57 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
58 57 a1i ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ∈ ( 0 [,) +∞ ) )
59 56 58 ifclda ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
60 59 ad2antrr ⊢ ( ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
61 fconstmpt ⊢ ( ℝ × { 𝑥 } ) = ( 𝑧 ∈ ℝ ↦ 𝑥 )
62 61 a1i ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ℝ × { 𝑥 } ) = ( 𝑧 ∈ ℝ ↦ 𝑥 ) )
63 eqidd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) )
64 47 49 60 62 63 offval2 ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( ℝ × { 𝑥 } ) ∘f · ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) = ( 𝑧 ∈ ℝ ↦ ( 𝑥 · if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) )
65 ovif2 ⊢ ( 𝑥 · if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) = if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , ( 𝑥 · 0 ) )
66 48 recnd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝑥 ∈ ℂ )
67 66 adantr ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → 𝑥 ∈ ℂ )
68 67 mul01d ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑥 · 0 ) = 0 )
69 68 ifeq2d ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , ( 𝑥 · 0 ) ) = if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
70 65 69 eqtrid ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑥 · if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) = if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
71 70 mpteq2dv ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑧 ∈ ℝ ↦ ( 𝑥 · if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
72 64 71 eqtrd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( ℝ × { 𝑥 } ) ∘f · ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
73 72 fveq2d ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( ( ℝ × { 𝑥 } ) ∘f · ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) = ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) )
74 59 adantr ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
75 74 fmpttd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
76 75 adantr ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
77 inss2 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺
78 77 a1i ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺 )
79 20 17 mbfdm2 ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol )
80 7 ffvelcdmda ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
81 7 feqmptd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 = ( 𝑧 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑧 ) ) )
82 simplr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → 𝐺 ∈ 𝐿1 )
83 81 82 eqeltrrd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ 𝐿1 )
84 78 79 80 83 iblss ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ 𝐿1 )
85 52 84 iblabs ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ 𝐿1 )
86 53 54 iblpos ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ 𝐿1 ↔ ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ∈ ℝ ) ) )
87 85 86 mpbid ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ∈ ℝ ) )
88 87 simprd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ∈ ℝ )
89 88 adantr ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ∈ ℝ )
90 simplrl ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → 𝑥 ∈ ℝ )
91 neq0 ⊢ ( ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ↔ ∃ 𝑧 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) )
92 0re ⊢ 0 ∈ ℝ
93 92 a1i ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ∈ ℝ )
94 elinel1 ⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑧 ∈ dom 𝐹 )
95 ffvelcdm ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
96 2 94 95 syl2an ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
97 96 abscld ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
98 simplrl ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 𝑥 ∈ ℝ )
99 96 absge0d ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
100 simprr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
101 2fveq3 ⊢ ( 𝑦 = 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
102 101 breq1d ⊢ ( 𝑦 = 𝑧 → ( ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ↔ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑥 ) )
103 102 rspccva ⊢ ( ( ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ∧ 𝑧 ∈ dom 𝐹 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑥 )
104 100 94 103 syl2an ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑥 )
105 93 97 98 99 104 letrd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ 𝑥 )
106 105 ex ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 0 ≤ 𝑥 ) )
107 106 exlimdv ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∃ 𝑧 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 0 ≤ 𝑥 ) )
108 91 107 biimtrid ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → 0 ≤ 𝑥 ) )
109 108 imp ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → 0 ≤ 𝑥 )
110 elrege0 ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
111 90 109 110 sylanbrc ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → 𝑥 ∈ ( 0 [,) +∞ ) )
112 76 89 111 itg2mulc ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( ( ℝ × { 𝑥 } ) ∘f · ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) = ( 𝑥 · ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) )
113 73 112 eqtr3d ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) = ( 𝑥 · ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) )
114 90 89 remulcld ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( 𝑥 · ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) , 0 ) ) ) ) ∈ ℝ )
115 113 114 eqeltrd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
116 115 ex ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ¬ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ ) )
117 noel ⊢ ¬ 𝑧 ∈ ∅
118 eleq2 ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↔ 𝑧 ∈ ∅ ) )
119 117 118 mtbiri ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) )
120 iffalse ⊢ ( ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = 0 )
121 119 120 syl ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = 0 )
122 121 mpteq2dv ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) = ( 𝑧 ∈ ℝ ↦ 0 ) )
123 fconstmpt ⊢ ( ℝ × { 0 } ) = ( 𝑧 ∈ ℝ ↦ 0 )
124 122 123 eqtr4di ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) = ( ℝ × { 0 } ) )
125 124 fveq2d ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( ℝ × { 0 } ) ) )
126 itg20 ⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0
127 126 92 eqeltri ⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) ∈ ℝ
128 125 127 eqeltrdi ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) = ∅ → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
129 116 128 pm2.61d2 ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
130 98 53 remulcld ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ )
131 130 rexrd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ* )
132 98 53 105 54 mulge0d ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → 0 ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
133 elxrge0 ⊢ ( ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ℝ* ∧ 0 ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) )
134 131 132 133 sylanbrc ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( 0 [,] +∞ ) )
135 134 42 ifclda ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
136 135 adantr ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
137 136 fmpttd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
138 96 52 absmuld ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
139 abscl ⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ℂ → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ )
140 absge0 ⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ℂ → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) )
141 139 140 jca ⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ℂ → ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
142 52 141 syl ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
143 lemul1a ⊢ ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
144 97 98 142 104 143 syl31anc ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
145 138 144 eqbrtrd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
146 iftrue ⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
147 146 adantl ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
148 iftrue ⊢ ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
149 148 adantl ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
150 145 147 149 3brtr4d ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
151 0le0 ⊢ 0 ≤ 0
152 151 a1i ⊢ ( ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 0 ≤ 0 )
153 iffalse ⊢ ( ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) = 0 )
154 152 153 120 3brtr4d ⊢ ( ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
155 154 adantl ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) ∧ ¬ 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
156 150 155 pm2.61dan ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
157 156 ralrimivw ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ∀ 𝑧 ∈ ℝ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) )
158 46 a1i ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ℝ ∈ V )
159 eqidd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
160 eqidd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) = ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
161 158 44 136 159 160 ofrfval2 ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ∘r ≤ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ↔ ∀ 𝑧 ∈ ℝ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ≤ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
162 157 161 mpbird ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ∘r ≤ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) )
163 itg2le ⊢ ( ( ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ∘r ≤ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) )
164 45 137 162 163 syl3anc ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) )
165 itg2lecl ⊢ ( ( ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( 𝑥 · ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
166 45 129 164 165 syl3anc ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ )
167 36 38 iblpos ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ 𝐿1 ↔ ( ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑧 ∈ ℝ ↦ if ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
168 35 166 167 mpbir2and ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ 𝐿1 )
169 17 20 168 iblabsr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝑧 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ 𝐿1 )
170 16 169 eqeltrd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝐿1 )
171 170 rexlimdvaa ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 → ( 𝐹 ∘f · 𝐺 ) ∈ 𝐿1 ) )
172 171 3impia ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( 𝐹 ∘f · 𝐺 ) ∈ 𝐿1 )