Theorem ulm0

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

	Ref	Expression
Hypotheses	ulm0.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	ulm0.m	$$⊢\phi \to M\in \mathbb{Z}$$
	ulm0.f	$$⊢\phi \to F:Z⟶{ℂ}^S$$
	ulm0.g	$$⊢\phi \to G:S⟶ℂ$$
Assertion	ulm0	$$⊢\left(\phi \wedge S=\varnothing \right)\to F\underset{u}{⇝}\left(S\right)G$$

Proof

Step	Hyp	Ref	Expression
1		ulm0.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		ulm0.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		ulm0.f	$$⊢\phi \to F:Z⟶{ℂ}^S$$
4		ulm0.g	$$⊢\phi \to G:S⟶ℂ$$
5		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
6	2 5	syl	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
7	6 1	eleqtrrdi	$$⊢\phi \to M\in Z$$
8	7	ne0d	$$⊢\phi \to Z\ne \varnothing$$
9		ral0	$$⊢\forall z\in \varnothing \left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x$$
10		simpr	$$⊢\left(\phi \wedge S=\varnothing \right)\to S=\varnothing$$
11	10	raleqdv	$$⊢\left(\phi \wedge S=\varnothing \right)\to \left(\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\leftrightarrow \forall z\in \varnothing \left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\right)$$
12	9 11	mpbiri	$$⊢\left(\phi \wedge S=\varnothing \right)\to \forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x$$
13	12	ralrimivw	$$⊢\left(\phi \wedge S=\varnothing \right)\to \forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x$$
14	13	ralrimivw	$$⊢\left(\phi \wedge S=\varnothing \right)\to \forall j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x$$
15		r19.2z	$$⊢\left(Z\ne \varnothing \wedge \forall j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x$$
16	8 14 15	syl2an2r	$$⊢\left(\phi \wedge S=\varnothing \right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x$$
17	16	ralrimivw	$$⊢\left(\phi \wedge S=\varnothing \right)\to \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x$$
18	2	adantr	$$⊢\left(\phi \wedge S=\varnothing \right)\to M\in \mathbb{Z}$$
19	3	adantr	$$⊢\left(\phi \wedge S=\varnothing \right)\to F:Z⟶{ℂ}^S$$
20		eqidd	$$⊢\left(\left(\phi \wedge S=\varnothing \right)\wedge \left(k\in Z\wedge z\in S\right)\right)\to F\left(k\right)\left(z\right)=F\left(k\right)\left(z\right)$$
21		eqidd	$$⊢\left(\left(\phi \wedge S=\varnothing \right)\wedge z\in S\right)\to G\left(z\right)=G\left(z\right)$$
22	4	adantr	$$⊢\left(\phi \wedge S=\varnothing \right)\to G:S⟶ℂ$$
23		0ex	$$⊢\varnothing \in \mathrm{V}$$
24	10 23	eqeltrdi	$$⊢\left(\phi \wedge S=\varnothing \right)\to S\in \mathrm{V}$$
25	1 18 19 20 21 22 24	ulm2	$$⊢\left(\phi \wedge S=\varnothing \right)\to \left(F\underset{u}{⇝}\left(S\right)G\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\right)$$
26	17 25	mpbird	$$⊢\left(\phi \wedge S=\varnothing \right)\to F\underset{u}{⇝}\left(S\right)G$$