Metamath Proof Explorer

Theorem iblulm

Description: A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses itgulm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
itgulm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
itgulm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝐿1 )
itgulm.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
itgulm.s ⊢ ( 𝜑 → ( vol ‘ 𝑆 ) ∈ ℝ )
Assertion iblulm ( 𝜑 → 𝐺 ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 itgulm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 itgulm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 itgulm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝐿1 )
4 itgulm.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
5 itgulm.s ⊢ ( 𝜑 → ( vol ‘ 𝑆 ) ∈ ℝ )
6 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
7 ulmf2 ⊢ ( ( 𝐹 Fn 𝑍 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
8 6 4 7 syl2anc ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
9 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
10 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
11 1rp ⊢ 1 ∈ ℝ+
12 11 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
13 1 2 8 9 10 4 12 ulmi ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 )
14 1 r19.2uz ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 )
15 13 14 syl ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 )
16 ulmcl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
17 4 16 syl ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
18 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → 𝐺 : 𝑆 ⟶ ℂ )
19 18 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → 𝐺 = ( 𝑧 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑧 ) ) )
20 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
21 elmapi ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
23 22 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
24 23 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
25 18 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
26 24 25 nncand ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝐺 ‘ 𝑧 ) )
27 26 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑧 ) ) )
28 19 27 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → 𝐺 = ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) )
29 23 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝑧 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
30 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐿1 )
31 30 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐿1 )
32 29 31 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( 𝑧 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ 𝐿1 )
33 24 25 subcld ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
34 ulmscl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝑆 ∈ V )
35 4 34 syl ⊢ ( 𝜑 → 𝑆 ∈ V )
36 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → 𝑆 ∈ V )
37 36 24 25 29 19 offval2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∘f − 𝐺 ) = ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) )
38 iblmbf ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝐿1 → ( 𝐹 ‘ 𝑘 ) ∈ MblFn )
39 31 38 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ MblFn )
40 iblmbf ⊢ ( 𝑥 ∈ 𝐿1 → 𝑥 ∈ MblFn )
41 40 ssriv ⊢ 𝐿1 ⊆ MblFn
42 fss ⊢ ( ( 𝐹 : 𝑍 ⟶ 𝐿1 ∧ 𝐿1 ⊆ MblFn ) → 𝐹 : 𝑍 ⟶ MblFn )
43 3 41 42 sylancl ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ MblFn )
44 1 2 43 4 mbfulm ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
45 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → 𝐺 ∈ MblFn )
46 39 45 mbfsub ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∘f − 𝐺 ) ∈ MblFn )
47 37 46 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn )
48 eqid ⊢ ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) )
49 48 33 dmmptd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) = 𝑆 )
50 49 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( vol ‘ dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) = ( vol ‘ 𝑆 ) )
51 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( vol ‘ 𝑆 ) ∈ ℝ )
52 50 51 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( vol ‘ dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ ℝ )
53 1re ⊢ 1 ∈ ℝ
54 22 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ∈ ℂ )
55 17 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐺 : 𝑆 ⟶ ℂ )
56 55 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
57 54 56 subcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
58 57 abscld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
59 ltle ⊢ ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ≤ 1 ) )
60 58 53 59 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ≤ 1 ) )
61 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
62 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑥 ) )
63 61 62 oveq12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
64 ovex ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ V
65 63 48 64 fvmpt ⊢ ( 𝑥 ∈ 𝑆 → ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
66 65 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
67 66 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) )
68 67 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 1 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ≤ 1 ) )
69 60 68 sylibrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 → ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 1 ) )
70 69 ralimdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 → ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 1 ) )
71 70 impr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 1 )
72 49 raleqdv ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( ∀ 𝑥 ∈ dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 1 ↔ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 1 ) )
73 71 72 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ∀ 𝑥 ∈ dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 1 )
74 brralrspcev ⊢ ( ( 1 ∈ ℝ ∧ ∀ 𝑥 ∈ dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 1 ) → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 𝑟 )
75 53 73 74 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 𝑟 )
76 bddibl ⊢ ( ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ∈ MblFn ∧ ( vol ‘ dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ ℝ ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑥 ∈ dom ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ( abs ‘ ( ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ‘ 𝑥 ) ) ≤ 𝑟 ) → ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ∈ 𝐿1 )
77 47 52 75 76 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ∈ 𝐿1 )
78 24 32 33 77 iblsub ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → ( 𝑧 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) ) ∈ 𝐿1 )
79 28 78 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ ∀ 𝑥 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 1 ) ) → 𝐺 ∈ 𝐿1 )
80 15 79 rexlimddv ⊢ ( 𝜑 → 𝐺 ∈ 𝐿1 )