ucnextcn

Description: Extension by continuity. Theorem 2 of BourbakiTop1 p. II.20. Given an uniform space on a set X , a subset A dense in X , and a function F uniformly continuous from A to Y , that function can be extended by continuity to the whole X , and its extension is uniformly continuous. (Contributed by Thierry Arnoux, 25-Jan-2018)

	Ref	Expression
Hypotheses	ucnextcn.x	$⊢ X = {Base}_{V}$
	ucnextcn.y	$⊢ Y = {Base}_{W}$
	ucnextcn.j	$⊢ J = TopOpen (V)$
	ucnextcn.k	$⊢ K = TopOpen (W)$
	ucnextcn.s	$⊢ S = UnifSt (V)$
	ucnextcn.t	$⊢ T = UnifSt (V ↾_{𝑠} A)$
	ucnextcn.u	$⊢ U = UnifSt (W)$
	ucnextcn.v	$⊢ φ \to V \in TopSp$
	ucnextcn.r	$⊢ φ \to V \in UnifSp$
	ucnextcn.w	$⊢ φ \to W \in TopSp$
	ucnextcn.z	$⊢ φ \to W \in CUnifSp$
	ucnextcn.h	$⊢ φ \to K \in Haus$
	ucnextcn.a	$⊢ φ \to A \subseteq X$
	ucnextcn.f	$⊢ φ \to F \in (T uCn U)$
	ucnextcn.c	$⊢ φ \to cls (J) (A) = X$
Assertion	ucnextcn	$⊢ φ \to (J CnExt K) (F) \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		ucnextcn.x	$⊢ X = {Base}_{V}$
2		ucnextcn.y	$⊢ Y = {Base}_{W}$
3		ucnextcn.j	$⊢ J = TopOpen (V)$
4		ucnextcn.k	$⊢ K = TopOpen (W)$
5		ucnextcn.s	$⊢ S = UnifSt (V)$
6		ucnextcn.t	$⊢ T = UnifSt (V ↾_{𝑠} A)$
7		ucnextcn.u	$⊢ U = UnifSt (W)$
8		ucnextcn.v	$⊢ φ \to V \in TopSp$
9		ucnextcn.r	$⊢ φ \to V \in UnifSp$
10		ucnextcn.w	$⊢ φ \to W \in TopSp$
11		ucnextcn.z	$⊢ φ \to W \in CUnifSp$
12		ucnextcn.h	$⊢ φ \to K \in Haus$
13		ucnextcn.a	$⊢ φ \to A \subseteq X$
14		ucnextcn.f	$⊢ φ \to F \in (T uCn U)$
15		ucnextcn.c	$⊢ φ \to cls (J) (A) = X$
16	1 6	ressust	$⊢ (V \in UnifSp \land A \subseteq X) \to T \in UnifOn (A)$
17	9 13 16	syl2anc	$⊢ φ \to T \in UnifOn (A)$
18		cuspusp	$⊢ W \in CUnifSp \to W \in UnifSp$
19	11 18	syl	$⊢ φ \to W \in UnifSp$
20	2 7 4	isusp	$⊢ W \in UnifSp \leftrightarrow (U \in UnifOn (Y) \land K = unifTop (U))$
21	19 20	sylib	$⊢ φ \to (U \in UnifOn (Y) \land K = unifTop (U))$
22	21	simpld	$⊢ φ \to U \in UnifOn (Y)$
23		isucn	$⊢ (T \in UnifOn (A) \land U \in UnifOn (Y)) \to (F \in (T uCn U) \leftrightarrow (F : A ⟶ Y \land \forall w \in U \exists v \in T \forall y \in A \forall z \in A (y v z \to F (y) w F (z))))$
24	17 22 23	syl2anc	$⊢ φ \to (F \in (T uCn U) \leftrightarrow (F : A ⟶ Y \land \forall w \in U \exists v \in T \forall y \in A \forall z \in A (y v z \to F (y) w F (z))))$
25	14 24	mpbid	$⊢ φ \to (F : A ⟶ Y \land \forall w \in U \exists v \in T \forall y \in A \forall z \in A (y v z \to F (y) w F (z)))$
26	25	simpld	$⊢ φ \to F : A ⟶ Y$
27	22	adantr	$⊢ (φ \land x \in X) \to U \in UnifOn (Y)$
28	27	elfvexd	$⊢ (φ \land x \in X) \to Y \in V$
29		simpr	$⊢ (φ \land x \in X) \to x \in X$
30	15	adantr	$⊢ (φ \land x \in X) \to cls (J) (A) = X$
31	29 30	eleqtrrd	$⊢ (φ \land x \in X) \to x \in cls (J) (A)$
32	1 3	istps	$⊢ V \in TopSp \leftrightarrow J \in TopOn (X)$
33	8 32	sylib	$⊢ φ \to J \in TopOn (X)$
34	33	adantr	$⊢ (φ \land x \in X) \to J \in TopOn (X)$
35	13	adantr	$⊢ (φ \land x \in X) \to A \subseteq X$
36		trnei	$⊢ (J \in TopOn (X) \land A \subseteq X \land x \in X) \to (x \in cls (J) (A) \leftrightarrow nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A))$
37	34 35 29 36	syl3anc	$⊢ (φ \land x \in X) \to (x \in cls (J) (A) \leftrightarrow nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A))$
38	31 37	mpbid	$⊢ (φ \land x \in X) \to nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A)$
39		filfbas	$⊢ nei (J) (\{x\}) ↾_{𝑡} A \in Fil (A) \to nei (J) (\{x\}) ↾_{𝑡} A \in fBas (A)$
40	38 39	syl	$⊢ (φ \land x \in X) \to nei (J) (\{x\}) ↾_{𝑡} A \in fBas (A)$
41	26	adantr	$⊢ (φ \land x \in X) \to F : A ⟶ Y$
42		fmval	$⊢ (Y \in V \land nei (J) (\{x\}) ↾_{𝑡} A \in fBas (A) \land F : A ⟶ Y) \to (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) = Y filGen ran (a \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [a])$
43	28 40 41 42	syl3anc	$⊢ (φ \land x \in X) \to (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) = Y filGen ran (a \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [a])$
44	17	adantr	$⊢ (φ \land x \in X) \to T \in UnifOn (A)$
45	14	adantr	$⊢ (φ \land x \in X) \to F \in (T uCn U)$
46	1 5 3	isusp	$⊢ V \in UnifSp \leftrightarrow (S \in UnifOn (X) \land J = unifTop (S))$
47	9 46	sylib	$⊢ φ \to (S \in UnifOn (X) \land J = unifTop (S))$
48	47	simpld	$⊢ φ \to S \in UnifOn (X)$
49	48	adantr	$⊢ (φ \land x \in X) \to S \in UnifOn (X)$
50	9	adantr	$⊢ (φ \land x \in X) \to V \in UnifSp$
51	8	adantr	$⊢ (φ \land x \in X) \to V \in TopSp$
52	1 3 5	neipcfilu	$⊢ (V \in UnifSp \land V \in TopSp \land x \in X) \to nei (J) (\{x\}) \in CauFilU (S)$
53	50 51 29 52	syl3anc	$⊢ (φ \land x \in X) \to nei (J) (\{x\}) \in CauFilU (S)$
54		0nelfb	$⊢ nei (J) (\{x\}) ↾_{𝑡} A \in fBas (A) \to \neg \emptyset \in (nei (J) (\{x\}) ↾_{𝑡} A)$
55	40 54	syl	$⊢ (φ \land x \in X) \to \neg \emptyset \in (nei (J) (\{x\}) ↾_{𝑡} A)$
56		trcfilu	$⊢ (S \in UnifOn (X) \land (nei (J) (\{x\}) \in CauFilU (S) \land \neg \emptyset \in (nei (J) (\{x\}) ↾_{𝑡} A)) \land A \subseteq X) \to nei (J) (\{x\}) ↾_{𝑡} A \in CauFilU (S ↾_{𝑡} (A \times A))$
57	49 53 55 35 56	syl121anc	$⊢ (φ \land x \in X) \to nei (J) (\{x\}) ↾_{𝑡} A \in CauFilU (S ↾_{𝑡} (A \times A))$
58	44	elfvexd	$⊢ (φ \land x \in X) \to A \in V$
59		ressuss	$⊢ A \in V \to UnifSt (V ↾_{𝑠} A) = UnifSt (V) ↾_{𝑡} (A \times A)$
60	5	oveq1i	$⊢ S ↾_{𝑡} (A \times A) = UnifSt (V) ↾_{𝑡} (A \times A)$
61	59 6 60	3eqtr4g	$⊢ A \in V \to T = S ↾_{𝑡} (A \times A)$
62	61	fveq2d	$⊢ A \in V \to CauFilU (T) = CauFilU (S ↾_{𝑡} (A \times A))$
63	58 62	syl	$⊢ (φ \land x \in X) \to CauFilU (T) = CauFilU (S ↾_{𝑡} (A \times A))$
64	57 63	eleqtrrd	$⊢ (φ \land x \in X) \to nei (J) (\{x\}) ↾_{𝑡} A \in CauFilU (T)$
65		imaeq2	$⊢ a = b \to F [a] = F [b]$
66	65	cbvmptv	$⊢ (a \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [a]) = (b \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [b])$
67	66	rneqi	$⊢ ran (a \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [a]) = ran (b \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [b])$
68	44 27 45 64 67	fmucnd	$⊢ (φ \land x \in X) \to ran (a \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [a]) \in CauFilU (U)$
69		cfilufg	$⊢ (U \in UnifOn (Y) \land ran (a \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [a]) \in CauFilU (U)) \to Y filGen ran (a \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [a]) \in CauFilU (U)$
70	27 68 69	syl2anc	$⊢ (φ \land x \in X) \to Y filGen ran (a \in (nei (J) (\{x\}) ↾_{𝑡} A) ⟼ F [a]) \in CauFilU (U)$
71	43 70	eqeltrd	$⊢ (φ \land x \in X) \to (Y FilMap F) (nei (J) (\{x\}) ↾_{𝑡} A) \in CauFilU (U)$
72	1 2 3 4 7 8 10 11 12 13 26 15 71	cnextucn	$⊢ φ \to (J CnExt K) (F) \in (J Cn K)$

Metamath Proof Explorer

Theorem ucnextcn

Proof