Metamath Proof Explorer

Theorem xkofvcn

Description: Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn .) (Contributed by Mario Carneiro, 20-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses xkofvcn.1 
|- X = U. R
xkofvcn.2 
|- F = ( f e. ( R Cn S ) , x e. X |-> ( f ` x ) )
Assertion xkofvcn 
|- ( ( R e. N-Locally Comp /\ S e. Top ) -> F e. ( ( ( S ^ko R ) tX R ) Cn S ) )

Proof

Step Hyp Ref Expression
1 xkofvcn.1 
 |-  X = U. R
2 xkofvcn.2 
 |-  F = ( f e. ( R Cn S ) , x e. X |-> ( f ` x ) )
3 nllytop 
 |-  ( R e. N-Locally Comp -> R e. Top )
4 eqid 
 |-  ( S ^ko R ) = ( S ^ko R )
5 4 xkotopon 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
6 3 5 sylan 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
7 3 adantr 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> R e. Top )
8 1 toptopon 
 |-  ( R e. Top <-> R e. ( TopOn ` X ) )
9 7 8 sylib 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> R e. ( TopOn ` X ) )
10 6 9 cnmpt1st 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( f e. ( R Cn S ) , x e. X |-> f ) e. ( ( ( S ^ko R ) tX R ) Cn ( S ^ko R ) ) )
11 6 9 cnmpt2nd 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( f e. ( R Cn S ) , x e. X |-> x ) e. ( ( ( S ^ko R ) tX R ) Cn R ) )
12 1on 
 |-  1o e. On
13 distopon 
 |-  ( 1o e. On -> ~P 1o e. ( TopOn ` 1o ) )
14 12 13 mp1i 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ~P 1o e. ( TopOn ` 1o ) )
15 xkoccn 
 |-  ( ( ~P 1o e. ( TopOn ` 1o ) /\ R e. ( TopOn ` X ) ) -> ( y e. X |-> ( 1o X. { y } ) ) e. ( R Cn ( R ^ko ~P 1o ) ) )
16 14 9 15 syl2anc 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( y e. X |-> ( 1o X. { y } ) ) e. ( R Cn ( R ^ko ~P 1o ) ) )
17 sneq 
 |-  ( y = x -> { y } = { x } )
18 17 xpeq2d 
 |-  ( y = x -> ( 1o X. { y } ) = ( 1o X. { x } ) )
19 6 9 11 9 16 18 cnmpt21 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( f e. ( R Cn S ) , x e. X |-> ( 1o X. { x } ) ) e. ( ( ( S ^ko R ) tX R ) Cn ( R ^ko ~P 1o ) ) )
20 distop 
 |-  ( 1o e. On -> ~P 1o e. Top )
21 12 20 mp1i 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ~P 1o e. Top )
22 eqid 
 |-  ( R ^ko ~P 1o ) = ( R ^ko ~P 1o )
23 22 xkotopon 
 |-  ( ( ~P 1o e. Top /\ R e. Top ) -> ( R ^ko ~P 1o ) e. ( TopOn ` ( ~P 1o Cn R ) ) )
24 21 7 23 syl2anc 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( R ^ko ~P 1o ) e. ( TopOn ` ( ~P 1o Cn R ) ) )
25 simpl 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> R e. N-Locally Comp )
26 simpr 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> S e. Top )
27 eqid 
 |-  ( g e. ( R Cn S ) , h e. ( ~P 1o Cn R ) |-> ( g o. h ) ) = ( g e. ( R Cn S ) , h e. ( ~P 1o Cn R ) |-> ( g o. h ) )
28 27 xkococn 
 |-  ( ( ~P 1o e. Top /\ R e. N-Locally Comp /\ S e. Top ) -> ( g e. ( R Cn S ) , h e. ( ~P 1o Cn R ) |-> ( g o. h ) ) e. ( ( ( S ^ko R ) tX ( R ^ko ~P 1o ) ) Cn ( S ^ko ~P 1o ) ) )
29 21 25 26 28 syl3anc 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( g e. ( R Cn S ) , h e. ( ~P 1o Cn R ) |-> ( g o. h ) ) e. ( ( ( S ^ko R ) tX ( R ^ko ~P 1o ) ) Cn ( S ^ko ~P 1o ) ) )
30 coeq1 
 |-  ( g = f -> ( g o. h ) = ( f o. h ) )
31 coeq2 
 |-  ( h = ( 1o X. { x } ) -> ( f o. h ) = ( f o. ( 1o X. { x } ) ) )
32 30 31 sylan9eq 
 |-  ( ( g = f /\ h = ( 1o X. { x } ) ) -> ( g o. h ) = ( f o. ( 1o X. { x } ) ) )
33 6 9 10 19 6 24 29 32 cnmpt22 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( f e. ( R Cn S ) , x e. X |-> ( f o. ( 1o X. { x } ) ) ) e. ( ( ( S ^ko R ) tX R ) Cn ( S ^ko ~P 1o ) ) )
34 eqid 
 |-  ( S ^ko ~P 1o ) = ( S ^ko ~P 1o )
35 34 xkotopon 
 |-  ( ( ~P 1o e. Top /\ S e. Top ) -> ( S ^ko ~P 1o ) e. ( TopOn ` ( ~P 1o Cn S ) ) )
36 21 26 35 syl2anc 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( S ^ko ~P 1o ) e. ( TopOn ` ( ~P 1o Cn S ) ) )
37 0lt1o 
 |-  (/) e. 1o
38 37 a1i 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> (/) e. 1o )
39 unipw 
 |-  U. ~P 1o = 1o
40 39 eqcomi 
 |-  1o = U. ~P 1o
41 40 xkopjcn 
 |-  ( ( ~P 1o e. Top /\ S e. Top /\ (/) e. 1o ) -> ( g e. ( ~P 1o Cn S ) |-> ( g ` (/) ) ) e. ( ( S ^ko ~P 1o ) Cn S ) )
42 21 26 38 41 syl3anc 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( g e. ( ~P 1o Cn S ) |-> ( g ` (/) ) ) e. ( ( S ^ko ~P 1o ) Cn S ) )
43 fveq1 
 |-  ( g = ( f o. ( 1o X. { x } ) ) -> ( g ` (/) ) = ( ( f o. ( 1o X. { x } ) ) ` (/) ) )
44 vex 
 |-  x e. _V
45 44 fconst 
 |-  ( 1o X. { x } ) : 1o --> { x }
46 fvco3 
 |-  ( ( ( 1o X. { x } ) : 1o --> { x } /\ (/) e. 1o ) -> ( ( f o. ( 1o X. { x } ) ) ` (/) ) = ( f ` ( ( 1o X. { x } ) ` (/) ) ) )
47 45 37 46 mp2an 
 |-  ( ( f o. ( 1o X. { x } ) ) ` (/) ) = ( f ` ( ( 1o X. { x } ) ` (/) ) )
48 44 fvconst2 
 |-  ( (/) e. 1o -> ( ( 1o X. { x } ) ` (/) ) = x )
49 37 48 ax-mp 
 |-  ( ( 1o X. { x } ) ` (/) ) = x
50 49 fveq2i 
 |-  ( f ` ( ( 1o X. { x } ) ` (/) ) ) = ( f ` x )
51 47 50 eqtri 
 |-  ( ( f o. ( 1o X. { x } ) ) ` (/) ) = ( f ` x )
52 43 51 eqtrdi 
 |-  ( g = ( f o. ( 1o X. { x } ) ) -> ( g ` (/) ) = ( f ` x ) )
53 6 9 33 36 42 52 cnmpt21 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> ( f e. ( R Cn S ) , x e. X |-> ( f ` x ) ) e. ( ( ( S ^ko R ) tX R ) Cn S ) )
54 2 53 eqeltrid 
 |-  ( ( R e. N-Locally Comp /\ S e. Top ) -> F e. ( ( ( S ^ko R ) tX R ) Cn S ) )