This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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