Metamath Proof Explorer


Theorem ulmuni

Description: A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017)

Ref Expression
Assertion ulmuni ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) → 𝐺 = 𝐻 )

Proof

Step Hyp Ref Expression
1 ulmcl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐺 : 𝑆 ⟶ ℂ )
2 1 adantr ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) → 𝐺 : 𝑆 ⟶ ℂ )
3 2 ffnd ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) → 𝐺 Fn 𝑆 )
4 ulmcl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐻𝐻 : 𝑆 ⟶ ℂ )
5 4 adantl ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) → 𝐻 : 𝑆 ⟶ ℂ )
6 5 ffnd ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) → 𝐻 Fn 𝑆 )
7 eqid ( ℤ𝑛 ) = ( ℤ𝑛 )
8 simplr ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑛 ∈ ℤ )
9 simpr ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
10 simpllr ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑥𝑆 )
11 fvex ( ℤ𝑛 ) ∈ V
12 11 mptex ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ∈ V
13 12 a1i ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ∈ V )
14 fveq2 ( 𝑖 = 𝑘 → ( 𝐹𝑖 ) = ( 𝐹𝑘 ) )
15 14 fveq1d ( 𝑖 = 𝑘 → ( ( 𝐹𝑖 ) ‘ 𝑥 ) = ( ( 𝐹𝑘 ) ‘ 𝑥 ) )
16 eqid ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) = ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) )
17 fvex ( ( 𝐹𝑘 ) ‘ 𝑥 ) ∈ V
18 15 16 17 fvmpt ( 𝑘 ∈ ( ℤ𝑛 ) → ( ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ‘ 𝑘 ) = ( ( 𝐹𝑘 ) ‘ 𝑥 ) )
19 18 eqcomd ( 𝑘 ∈ ( ℤ𝑛 ) → ( ( 𝐹𝑘 ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ‘ 𝑘 ) )
20 19 adantl ( ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) ∧ 𝑘 ∈ ( ℤ𝑛 ) ) → ( ( 𝐹𝑘 ) ‘ 𝑥 ) = ( ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ‘ 𝑘 ) )
21 simp-4l ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝐹 ( ⇝𝑢𝑆 ) 𝐺 )
22 7 8 9 10 13 20 21 ulmclm ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ⇝ ( 𝐺𝑥 ) )
23 simp-4r ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝐹 ( ⇝𝑢𝑆 ) 𝐻 )
24 7 8 9 10 13 20 23 ulmclm ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ⇝ ( 𝐻𝑥 ) )
25 climuni ( ( ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ⇝ ( 𝐺𝑥 ) ∧ ( 𝑖 ∈ ( ℤ𝑛 ) ↦ ( ( 𝐹𝑖 ) ‘ 𝑥 ) ) ⇝ ( 𝐻𝑥 ) ) → ( 𝐺𝑥 ) = ( 𝐻𝑥 ) )
26 22 24 25 syl2anc ( ( ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) ∧ 𝑛 ∈ ℤ ) ∧ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( 𝐺𝑥 ) = ( 𝐻𝑥 ) )
27 ulmf ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 → ∃ 𝑛 ∈ ℤ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
28 27 ad2antrr ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) → ∃ 𝑛 ∈ ℤ 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
29 26 28 r19.29a ( ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) ∧ 𝑥𝑆 ) → ( 𝐺𝑥 ) = ( 𝐻𝑥 ) )
30 3 6 29 eqfnfvd ( ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐹 ( ⇝𝑢𝑆 ) 𝐻 ) → 𝐺 = 𝐻 )