Metamath Proof Explorer


Theorem ulmclm

Description: A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015)

Ref Expression
Hypotheses ulmclm.z 𝑍 = ( ℤ𝑀 )
ulmclm.m ( 𝜑𝑀 ∈ ℤ )
ulmclm.f ( 𝜑𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
ulmclm.a ( 𝜑𝐴𝑆 )
ulmclm.h ( 𝜑𝐻𝑊 )
ulmclm.e ( ( 𝜑𝑘𝑍 ) → ( ( 𝐹𝑘 ) ‘ 𝐴 ) = ( 𝐻𝑘 ) )
ulmclm.u ( 𝜑𝐹 ( ⇝𝑢𝑆 ) 𝐺 )
Assertion ulmclm ( 𝜑𝐻 ⇝ ( 𝐺𝐴 ) )

Proof

Step Hyp Ref Expression
1 ulmclm.z 𝑍 = ( ℤ𝑀 )
2 ulmclm.m ( 𝜑𝑀 ∈ ℤ )
3 ulmclm.f ( 𝜑𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
4 ulmclm.a ( 𝜑𝐴𝑆 )
5 ulmclm.h ( 𝜑𝐻𝑊 )
6 ulmclm.e ( ( 𝜑𝑘𝑍 ) → ( ( 𝐹𝑘 ) ‘ 𝐴 ) = ( 𝐻𝑘 ) )
7 ulmclm.u ( 𝜑𝐹 ( ⇝𝑢𝑆 ) 𝐺 )
8 fveq2 ( 𝑧 = 𝐴 → ( ( 𝐹𝑘 ) ‘ 𝑧 ) = ( ( 𝐹𝑘 ) ‘ 𝐴 ) )
9 fveq2 ( 𝑧 = 𝐴 → ( 𝐺𝑧 ) = ( 𝐺𝐴 ) )
10 8 9 oveq12d ( 𝑧 = 𝐴 → ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) = ( ( ( 𝐹𝑘 ) ‘ 𝐴 ) − ( 𝐺𝐴 ) ) )
11 10 fveq2d ( 𝑧 = 𝐴 → ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝐴 ) − ( 𝐺𝐴 ) ) ) )
12 11 breq1d ( 𝑧 = 𝐴 → ( ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝐴 ) − ( 𝐺𝐴 ) ) ) < 𝑥 ) )
13 12 rspcv ( 𝐴𝑆 → ( ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 → ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝐴 ) − ( 𝐺𝐴 ) ) ) < 𝑥 ) )
14 4 13 syl ( 𝜑 → ( ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 → ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝐴 ) − ( 𝐺𝐴 ) ) ) < 𝑥 ) )
15 14 ralimdv ( 𝜑 → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝐴 ) − ( 𝐺𝐴 ) ) ) < 𝑥 ) )
16 15 reximdv ( 𝜑 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝐴 ) − ( 𝐺𝐴 ) ) ) < 𝑥 ) )
17 16 ralimdv ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝐴 ) − ( 𝐺𝐴 ) ) ) < 𝑥 ) )
18 eqidd ( ( 𝜑 ∧ ( 𝑘𝑍𝑧𝑆 ) ) → ( ( 𝐹𝑘 ) ‘ 𝑧 ) = ( ( 𝐹𝑘 ) ‘ 𝑧 ) )
19 eqidd ( ( 𝜑𝑧𝑆 ) → ( 𝐺𝑧 ) = ( 𝐺𝑧 ) )
20 ulmcl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐺 : 𝑆 ⟶ ℂ )
21 7 20 syl ( 𝜑𝐺 : 𝑆 ⟶ ℂ )
22 ulmscl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝑆 ∈ V )
23 7 22 syl ( 𝜑𝑆 ∈ V )
24 1 2 3 18 19 21 23 ulm2 ( 𝜑 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) )
25 6 eqcomd ( ( 𝜑𝑘𝑍 ) → ( 𝐻𝑘 ) = ( ( 𝐹𝑘 ) ‘ 𝐴 ) )
26 21 4 ffvelrnd ( 𝜑 → ( 𝐺𝐴 ) ∈ ℂ )
27 3 ffvelrnda ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
28 elmapi ( ( 𝐹𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹𝑘 ) : 𝑆 ⟶ ℂ )
29 27 28 syl ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) : 𝑆 ⟶ ℂ )
30 4 adantr ( ( 𝜑𝑘𝑍 ) → 𝐴𝑆 )
31 29 30 ffvelrnd ( ( 𝜑𝑘𝑍 ) → ( ( 𝐹𝑘 ) ‘ 𝐴 ) ∈ ℂ )
32 1 2 5 25 26 31 clim2c ( 𝜑 → ( 𝐻 ⇝ ( 𝐺𝐴 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝐴 ) − ( 𝐺𝐴 ) ) ) < 𝑥 ) )
33 17 24 32 3imtr4d ( 𝜑 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐻 ⇝ ( 𝐺𝐴 ) ) )
34 7 33 mpd ( 𝜑𝐻 ⇝ ( 𝐺𝐴 ) )