Metamath Proof Explorer

Theorem ulm0

Description: Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses ulm0.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulm0.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulm0.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
ulm0.g ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
Assertion ulm0 ( ( 𝜑 ∧ 𝑆 = ∅ ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 ulm0.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulm0.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 ulm0.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
4 ulm0.g ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
5 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 2 5 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
7 6 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
8 7 ne0d ⊢ ( 𝜑 → 𝑍 ≠ ∅ )
9 ral0 ⊢ ∀ 𝑧 ∈ ∅ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥
10 simpr ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → 𝑆 = ∅ )
11 10 raleqdv ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ ∅ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
12 9 11 mpbiri ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
13 12 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
14 13 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → ∀ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
15 r19.2z ⊢ ( ( 𝑍 ≠ ∅ ∧ ∀ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
16 8 14 15 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
17 16 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
18 2 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → 𝑀 ∈ ℤ )
19 3 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
20 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑆 = ∅ ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
21 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑆 = ∅ ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
22 4 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → 𝐺 : 𝑆 ⟶ ℂ )
23 0ex ⊢ ∅ ∈ V
24 10 23 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → 𝑆 ∈ V )
25 1 18 19 20 21 22 24 ulm2 ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
26 17 25 mpbird ⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )