Metamath Proof Explorer


Theorem xkopjcn

Description: Continuity of a projection map from the space of continuous functions. (This theorem can be strengthened, to joint continuity in both f and A as a function on ( S ^ko R ) tX R , but not without stronger assumptions on R ; see xkofvcn .) (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis xkopjcn.1 X=R
Assertion xkopjcn RTopSTopAXfRCnSfAS^koRCnS

Proof

Step Hyp Ref Expression
1 xkopjcn.1 X=R
2 eqid S^koR=S^koR
3 2 xkotopon RTopSTopS^koRTopOnRCnS
4 3 3adant3 RTopSTopAXS^koRTopOnRCnS
5 1 topopn RTopXR
6 5 3ad2ant1 RTopSTopAXXR
7 fconst6g STopX×S:XTop
8 7 3ad2ant2 RTopSTopAXX×S:XTop
9 pttop XRX×S:XTop𝑡X×STop
10 6 8 9 syl2anc RTopSTopAX𝑡X×STop
11 eqid S=S
12 1 11 cnf fRCnSf:XS
13 uniexg STopSV
14 13 3ad2ant2 RTopSTopAXSV
15 14 6 elmapd RTopSTopAXfSXf:XS
16 12 15 syl5ibr RTopSTopAXfRCnSfSX
17 16 ssrdv RTopSTopAXRCnSSX
18 simp2 RTopSTopAXSTop
19 eqid 𝑡X×S=𝑡X×S
20 19 11 ptuniconst XRSTopSX=𝑡X×S
21 6 18 20 syl2anc RTopSTopAXSX=𝑡X×S
22 17 21 sseqtrd RTopSTopAXRCnS𝑡X×S
23 eqid 𝑡X×S=𝑡X×S
24 23 restuni 𝑡X×STopRCnS𝑡X×SRCnS=𝑡X×S𝑡RCnS
25 10 22 24 syl2anc RTopSTopAXRCnS=𝑡X×S𝑡RCnS
26 25 fveq2d RTopSTopAXTopOnRCnS=TopOn𝑡X×S𝑡RCnS
27 4 26 eleqtrd RTopSTopAXS^koRTopOn𝑡X×S𝑡RCnS
28 1 19 xkoptsub RTopSTop𝑡X×S𝑡RCnSS^koR
29 28 3adant3 RTopSTopAX𝑡X×S𝑡RCnSS^koR
30 eqid 𝑡X×S𝑡RCnS=𝑡X×S𝑡RCnS
31 30 cnss1 S^koRTopOn𝑡X×S𝑡RCnS𝑡X×S𝑡RCnSS^koR𝑡X×S𝑡RCnSCnSS^koRCnS
32 27 29 31 syl2anc RTopSTopAX𝑡X×S𝑡RCnSCnSS^koRCnS
33 22 resmptd RTopSTopAXf𝑡X×SfARCnS=fRCnSfA
34 simp3 RTopSTopAXAX
35 23 19 ptpjcn XRX×S:XTopAXf𝑡X×SfA𝑡X×SCnX×SA
36 6 8 34 35 syl3anc RTopSTopAXf𝑡X×SfA𝑡X×SCnX×SA
37 fvconst2g STopAXX×SA=S
38 37 3adant1 RTopSTopAXX×SA=S
39 38 oveq2d RTopSTopAX𝑡X×SCnX×SA=𝑡X×SCnS
40 36 39 eleqtrd RTopSTopAXf𝑡X×SfA𝑡X×SCnS
41 23 cnrest f𝑡X×SfA𝑡X×SCnSRCnS𝑡X×Sf𝑡X×SfARCnS𝑡X×S𝑡RCnSCnS
42 40 22 41 syl2anc RTopSTopAXf𝑡X×SfARCnS𝑡X×S𝑡RCnSCnS
43 33 42 eqeltrrd RTopSTopAXfRCnSfA𝑡X×S𝑡RCnSCnS
44 32 43 sseldd RTopSTopAXfRCnSfAS^koRCnS