Metamath Proof Explorer


Theorem xkoco2cn

Description: If F is a continuous function, then g |-> F o. g is a continuous function on function spaces. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypotheses xkoco2cn.r φ R Top
xkoco2cn.f φ F S Cn T
Assertion xkoco2cn φ g R Cn S F g S ^ ko R Cn T ^ ko R

Proof

Step Hyp Ref Expression
1 xkoco2cn.r φ R Top
2 xkoco2cn.f φ F S Cn T
3 simpr φ g R Cn S g R Cn S
4 2 adantr φ g R Cn S F S Cn T
5 cnco g R Cn S F S Cn T F g R Cn T
6 3 4 5 syl2anc φ g R Cn S F g R Cn T
7 6 fmpttd φ g R Cn S F g : R Cn S R Cn T
8 eqid R = R
9 eqid y 𝒫 R | R 𝑡 y Comp = y 𝒫 R | R 𝑡 y Comp
10 eqid k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v = k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v
11 8 9 10 xkobval ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v = x | k 𝒫 R v T R 𝑡 k Comp x = h R Cn T | h k v
12 11 abeq2i x ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v k 𝒫 R v T R 𝑡 k Comp x = h R Cn T | h k v
13 simpr φ k 𝒫 R v T R 𝑡 k Comp g R Cn S g R Cn S
14 2 ad3antrrr φ k 𝒫 R v T R 𝑡 k Comp g R Cn S F S Cn T
15 13 14 5 syl2anc φ k 𝒫 R v T R 𝑡 k Comp g R Cn S F g R Cn T
16 imaeq1 h = F g h k = F g k
17 imaco F g k = F g k
18 16 17 eqtrdi h = F g h k = F g k
19 18 sseq1d h = F g h k v F g k v
20 19 elrab3 F g R Cn T F g h R Cn T | h k v F g k v
21 15 20 syl φ k 𝒫 R v T R 𝑡 k Comp g R Cn S F g h R Cn T | h k v F g k v
22 eqid S = S
23 eqid T = T
24 22 23 cnf F S Cn T F : S T
25 2 24 syl φ F : S T
26 25 ad3antrrr φ k 𝒫 R v T R 𝑡 k Comp g R Cn S F : S T
27 26 ffund φ k 𝒫 R v T R 𝑡 k Comp g R Cn S Fun F
28 imassrn g k ran g
29 8 22 cnf g R Cn S g : R S
30 13 29 syl φ k 𝒫 R v T R 𝑡 k Comp g R Cn S g : R S
31 30 frnd φ k 𝒫 R v T R 𝑡 k Comp g R Cn S ran g S
32 28 31 sstrid φ k 𝒫 R v T R 𝑡 k Comp g R Cn S g k S
33 26 fdmd φ k 𝒫 R v T R 𝑡 k Comp g R Cn S dom F = S
34 32 33 sseqtrrd φ k 𝒫 R v T R 𝑡 k Comp g R Cn S g k dom F
35 funimass3 Fun F g k dom F F g k v g k F -1 v
36 27 34 35 syl2anc φ k 𝒫 R v T R 𝑡 k Comp g R Cn S F g k v g k F -1 v
37 21 36 bitrd φ k 𝒫 R v T R 𝑡 k Comp g R Cn S F g h R Cn T | h k v g k F -1 v
38 37 rabbidva φ k 𝒫 R v T R 𝑡 k Comp g R Cn S | F g h R Cn T | h k v = g R Cn S | g k F -1 v
39 1 ad2antrr φ k 𝒫 R v T R 𝑡 k Comp R Top
40 cntop1 F S Cn T S Top
41 2 40 syl φ S Top
42 41 ad2antrr φ k 𝒫 R v T R 𝑡 k Comp S Top
43 simplrl φ k 𝒫 R v T R 𝑡 k Comp k 𝒫 R
44 43 elpwid φ k 𝒫 R v T R 𝑡 k Comp k R
45 simpr φ k 𝒫 R v T R 𝑡 k Comp R 𝑡 k Comp
46 2 ad2antrr φ k 𝒫 R v T R 𝑡 k Comp F S Cn T
47 simplrr φ k 𝒫 R v T R 𝑡 k Comp v T
48 cnima F S Cn T v T F -1 v S
49 46 47 48 syl2anc φ k 𝒫 R v T R 𝑡 k Comp F -1 v S
50 8 39 42 44 45 49 xkoopn φ k 𝒫 R v T R 𝑡 k Comp g R Cn S | g k F -1 v S ^ ko R
51 38 50 eqeltrd φ k 𝒫 R v T R 𝑡 k Comp g R Cn S | F g h R Cn T | h k v S ^ ko R
52 imaeq2 x = h R Cn T | h k v g R Cn S F g -1 x = g R Cn S F g -1 h R Cn T | h k v
53 eqid g R Cn S F g = g R Cn S F g
54 53 mptpreima g R Cn S F g -1 h R Cn T | h k v = g R Cn S | F g h R Cn T | h k v
55 52 54 eqtrdi x = h R Cn T | h k v g R Cn S F g -1 x = g R Cn S | F g h R Cn T | h k v
56 55 eleq1d x = h R Cn T | h k v g R Cn S F g -1 x S ^ ko R g R Cn S | F g h R Cn T | h k v S ^ ko R
57 51 56 syl5ibrcom φ k 𝒫 R v T R 𝑡 k Comp x = h R Cn T | h k v g R Cn S F g -1 x S ^ ko R
58 57 expimpd φ k 𝒫 R v T R 𝑡 k Comp x = h R Cn T | h k v g R Cn S F g -1 x S ^ ko R
59 58 rexlimdvva φ k 𝒫 R v T R 𝑡 k Comp x = h R Cn T | h k v g R Cn S F g -1 x S ^ ko R
60 12 59 syl5bi φ x ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v g R Cn S F g -1 x S ^ ko R
61 60 ralrimiv φ x ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v g R Cn S F g -1 x S ^ ko R
62 eqid S ^ ko R = S ^ ko R
63 62 xkotopon R Top S Top S ^ ko R TopOn R Cn S
64 1 41 63 syl2anc φ S ^ ko R TopOn R Cn S
65 ovex R Cn T V
66 65 pwex 𝒫 R Cn T V
67 8 9 10 xkotf k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v : y 𝒫 R | R 𝑡 y Comp × T 𝒫 R Cn T
68 frn k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v : y 𝒫 R | R 𝑡 y Comp × T 𝒫 R Cn T ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v 𝒫 R Cn T
69 67 68 ax-mp ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v 𝒫 R Cn T
70 66 69 ssexi ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v V
71 70 a1i φ ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v V
72 cntop2 F S Cn T T Top
73 2 72 syl φ T Top
74 8 9 10 xkoval R Top T Top T ^ ko R = topGen fi ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v
75 1 73 74 syl2anc φ T ^ ko R = topGen fi ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v
76 eqid T ^ ko R = T ^ ko R
77 76 xkotopon R Top T Top T ^ ko R TopOn R Cn T
78 1 73 77 syl2anc φ T ^ ko R TopOn R Cn T
79 64 71 75 78 subbascn φ g R Cn S F g S ^ ko R Cn T ^ ko R g R Cn S F g : R Cn S R Cn T x ran k y 𝒫 R | R 𝑡 y Comp , v T h R Cn T | h k v g R Cn S F g -1 x S ^ ko R
80 7 61 79 mpbir2and φ g R Cn S F g S ^ ko R Cn T ^ ko R