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 = R
xkofvcn.2 F = f R Cn S , x X f x
Assertion xkofvcn R N-Locally Comp S Top F S ^ ko R × t R Cn S

Proof

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