ulmuni

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

		Ref	Expression
	Assertion	ulmuni	$⊢ (F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \to G = H$

Proof

Step	Hyp	Ref	Expression
1		ulmcl	$⊢ F \underset{u}{⇝} (S) G \to G : S ⟶ ℂ$
2	1	adantr	$⊢ (F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \to G : S ⟶ ℂ$
3	2	ffnd	$⊢ (F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \to G Fn S$
4		ulmcl	$⊢ F \underset{u}{⇝} (S) H \to H : S ⟶ ℂ$
5	4	adantl	$⊢ (F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \to H : S ⟶ ℂ$
6	5	ffnd	$⊢ (F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \to H Fn S$
7		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
8		simplr	$⊢ ((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to n \in ℤ$
9		simpr	$⊢ ((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to F : ℤ_{\geq n} ⟶ ℂ^{S}$
10		simpllr	$⊢ ((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to x \in S$
11		fvex	$⊢ ℤ_{\geq n} \in V$
12	11	mptex	$⊢ (i \in ℤ_{\geq n} ⟼ F (i) (x)) \in V$
13	12	a1i	$⊢ ((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to (i \in ℤ_{\geq n} ⟼ F (i) (x)) \in V$
14		fveq2	$⊢ i = k \to F (i) = F (k)$
15	14	fveq1d	$⊢ i = k \to F (i) (x) = F (k) (x)$
16		eqid	$⊢ (i \in ℤ_{\geq n} ⟼ F (i) (x)) = (i \in ℤ_{\geq n} ⟼ F (i) (x))$
17		fvex	$⊢ F (k) (x) \in V$
18	15 16 17	fvmpt	$⊢ k \in ℤ_{\geq n} \to (i \in ℤ_{\geq n} ⟼ F (i) (x)) (k) = F (k) (x)$
19	18	eqcomd	$⊢ k \in ℤ_{\geq n} \to F (k) (x) = (i \in ℤ_{\geq n} ⟼ F (i) (x)) (k)$
20	19	adantl	$⊢ (((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \land k \in ℤ_{\geq n}) \to F (k) (x) = (i \in ℤ_{\geq n} ⟼ F (i) (x)) (k)$
21		simp-4l	$⊢ ((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to F \underset{u}{⇝} (S) G$
22	7 8 9 10 13 20 21	ulmclm	$⊢ ((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to (i \in ℤ_{\geq n} ⟼ F (i) (x)) ⇝ G (x)$
23		simp-4r	$⊢ ((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to F \underset{u}{⇝} (S) H$
24	7 8 9 10 13 20 23	ulmclm	$⊢ ((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to (i \in ℤ_{\geq n} ⟼ F (i) (x)) ⇝ H (x)$
25		climuni	$⊢ ((i \in ℤ_{\geq n} ⟼ F (i) (x)) ⇝ G (x) \land (i \in ℤ_{\geq n} ⟼ F (i) (x)) ⇝ H (x)) \to G (x) = H (x)$
26	22 24 25	syl2anc	$⊢ ((((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \land n \in ℤ) \land F : ℤ_{\geq n} ⟶ ℂ^{S}) \to G (x) = H (x)$
27		ulmf	$⊢ F \underset{u}{⇝} (S) G \to \exists n \in ℤ F : ℤ_{\geq n} ⟶ ℂ^{S}$
28	27	ad2antrr	$⊢ ((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \to \exists n \in ℤ F : ℤ_{\geq n} ⟶ ℂ^{S}$
29	26 28	r19.29a	$⊢ ((F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \land x \in S) \to G (x) = H (x)$
30	3 6 29	eqfnfvd	$⊢ (F \underset{u}{⇝} (S) G \land F \underset{u}{⇝} (S) H) \to G = H$

Metamath Proof Explorer

Theorem ulmuni

Proof