Metamath Proof Explorer


Theorem 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 φ V TopSp
ucnextcn.r φ V UnifSp
ucnextcn.w φ W TopSp
ucnextcn.z φ W CUnifSp
ucnextcn.h φ K Haus
ucnextcn.a φ A X
ucnextcn.f φ F T uCn U
ucnextcn.c φ cls J A = X
Assertion ucnextcn φ J CnExt K F 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 φ V TopSp
9 ucnextcn.r φ V UnifSp
10 ucnextcn.w φ W TopSp
11 ucnextcn.z φ W CUnifSp
12 ucnextcn.h φ K Haus
13 ucnextcn.a φ A X
14 ucnextcn.f φ F T uCn U
15 ucnextcn.c φ cls J A = X
16 1 6 ressust V UnifSp A X T UnifOn A
17 9 13 16 syl2anc φ T UnifOn A
18 cuspusp W CUnifSp W UnifSp
19 11 18 syl φ W UnifSp
20 2 7 4 isusp W UnifSp U UnifOn Y K = unifTop U
21 19 20 sylib φ U UnifOn Y K = unifTop U
22 21 simpld φ U UnifOn Y
23 isucn T UnifOn A U UnifOn Y F T uCn U F : A Y w U v T y A z A y v z F y w F z
24 17 22 23 syl2anc φ F T uCn U F : A Y w U v T y A z A y v z F y w F z
25 14 24 mpbid φ F : A Y w U v T y A z A y v z F y w F z
26 25 simpld φ F : A Y
27 22 adantr φ x X U UnifOn Y
28 27 elfvexd φ x X Y V
29 simpr φ x X x X
30 15 adantr φ x X cls J A = X
31 29 30 eleqtrrd φ x X x cls J A
32 1 3 istps V TopSp J TopOn X
33 8 32 sylib φ J TopOn X
34 33 adantr φ x X J TopOn X
35 13 adantr φ x X A X
36 trnei J TopOn X A X x X x cls J A nei J x 𝑡 A Fil A
37 34 35 29 36 syl3anc φ x X x cls J A nei J x 𝑡 A Fil A
38 31 37 mpbid φ x X nei J x 𝑡 A Fil A
39 filfbas nei J x 𝑡 A Fil A nei J x 𝑡 A fBas A
40 38 39 syl φ x X nei J x 𝑡 A fBas A
41 26 adantr φ x X F : A Y
42 fmval Y V nei J x 𝑡 A fBas A F : A Y Y FilMap F nei J x 𝑡 A = Y filGen ran a nei J x 𝑡 A F a
43 28 40 41 42 syl3anc φ x X Y FilMap F nei J x 𝑡 A = Y filGen ran a nei J x 𝑡 A F a
44 17 adantr φ x X T UnifOn A
45 14 adantr φ x X F T uCn U
46 1 5 3 isusp V UnifSp S UnifOn X J = unifTop S
47 9 46 sylib φ S UnifOn X J = unifTop S
48 47 simpld φ S UnifOn X
49 48 adantr φ x X S UnifOn X
50 9 adantr φ x X V UnifSp
51 8 adantr φ x X V TopSp
52 1 3 5 neipcfilu V UnifSp V TopSp x X nei J x CauFilU S
53 50 51 29 52 syl3anc φ x X nei J x CauFilU S
54 0nelfb nei J x 𝑡 A fBas A ¬ nei J x 𝑡 A
55 40 54 syl φ x X ¬ nei J x 𝑡 A
56 trcfilu S UnifOn X nei J x CauFilU S ¬ nei J x 𝑡 A A X nei J x 𝑡 A CauFilU S 𝑡 A × A
57 49 53 55 35 56 syl121anc φ x X nei J x 𝑡 A CauFilU S 𝑡 A × A
58 44 elfvexd φ x X A V
59 ressuss A V UnifSt V 𝑠 A = UnifSt V 𝑡 A × A
60 5 oveq1i S 𝑡 A × A = UnifSt V 𝑡 A × A
61 59 6 60 3eqtr4g A V T = S 𝑡 A × A
62 61 fveq2d A V CauFilU T = CauFilU S 𝑡 A × A
63 58 62 syl φ x X CauFilU T = CauFilU S 𝑡 A × A
64 57 63 eleqtrrd φ x X nei J x 𝑡 A CauFilU T
65 imaeq2 a = b F a = F b
66 65 cbvmptv a nei J x 𝑡 A F a = b nei J x 𝑡 A F b
67 66 rneqi ran a nei J x 𝑡 A F a = ran b nei J x 𝑡 A F b
68 44 27 45 64 67 fmucnd φ x X ran a nei J x 𝑡 A F a CauFilU U
69 cfilufg U UnifOn Y ran a nei J x 𝑡 A F a CauFilU U Y filGen ran a nei J x 𝑡 A F a CauFilU U
70 27 68 69 syl2anc φ x X Y filGen ran a nei J x 𝑡 A F a CauFilU U
71 43 70 eqeltrd φ x X Y FilMap F nei J x 𝑡 A CauFilU U
72 1 2 3 4 7 8 10 11 12 13 26 15 71 cnextucn φ J CnExt K F J Cn K