Metamath Proof Explorer


Theorem xkohmeo

Description: The Exponential Law for topological spaces. The "currying" function F is a homeomorphism on function spaces when J and K are exponentiable spaces (by xkococn , it is sufficient to assume that J , K are locally compact to ensure exponentiability). (Contributed by Mario Carneiro, 13-Apr-2015) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses xkohmeo.x φ J TopOn X
xkohmeo.y φ K TopOn Y
xkohmeo.f F = f J × t K Cn L x X y Y x f y
xkohmeo.j φ J N-Locally Comp
xkohmeo.k φ K N-Locally Comp
xkohmeo.l φ L Top
Assertion xkohmeo φ F L ^ ko J × t K Homeo L ^ ko K ^ ko J

Proof

Step Hyp Ref Expression
1 xkohmeo.x φ J TopOn X
2 xkohmeo.y φ K TopOn Y
3 xkohmeo.f F = f J × t K Cn L x X y Y x f y
4 xkohmeo.j φ J N-Locally Comp
5 xkohmeo.k φ K N-Locally Comp
6 xkohmeo.l φ L Top
7 txtopon J TopOn X K TopOn Y J × t K TopOn X × Y
8 1 2 7 syl2anc φ J × t K TopOn X × Y
9 topontop J × t K TopOn X × Y J × t K Top
10 8 9 syl φ J × t K Top
11 eqid L ^ ko J × t K = L ^ ko J × t K
12 11 xkotopon J × t K Top L Top L ^ ko J × t K TopOn J × t K Cn L
13 10 6 12 syl2anc φ L ^ ko J × t K TopOn J × t K Cn L
14 vex f V
15 vex x V
16 14 15 op1std z = f x 1 st z = f
17 14 15 op2ndd z = f x 2 nd z = x
18 eqidd z = f x y = y
19 16 17 18 oveq123d z = f x 2 nd z 1 st z y = x f y
20 19 mpteq2dv z = f x y Y 2 nd z 1 st z y = y Y x f y
21 20 mpompt z J × t K Cn L × X y Y 2 nd z 1 st z y = f J × t K Cn L , x X y Y x f y
22 txtopon L ^ ko J × t K TopOn J × t K Cn L J TopOn X L ^ ko J × t K × t J TopOn J × t K Cn L × X
23 13 1 22 syl2anc φ L ^ ko J × t K × t J TopOn J × t K Cn L × X
24 vex z V
25 vex y V
26 24 25 op1std w = z y 1 st w = z
27 26 fveq2d w = z y 1 st 1 st w = 1 st z
28 26 fveq2d w = z y 2 nd 1 st w = 2 nd z
29 24 25 op2ndd w = z y 2 nd w = y
30 27 28 29 oveq123d w = z y 2 nd 1 st w 1 st 1 st w 2 nd w = 2 nd z 1 st z y
31 30 mpompt w J × t K Cn L × X × Y 2 nd 1 st w 1 st 1 st w 2 nd w = z J × t K Cn L × X , y Y 2 nd z 1 st z y
32 txtopon L ^ ko J × t K × t J TopOn J × t K Cn L × X K TopOn Y L ^ ko J × t K × t J × t K TopOn J × t K Cn L × X × Y
33 23 2 32 syl2anc φ L ^ ko J × t K × t J × t K TopOn J × t K Cn L × X × Y
34 toptopon2 L Top L TopOn L
35 6 34 sylib φ L TopOn L
36 txcmp x Comp y Comp x × t y Comp
37 36 txnlly J N-Locally Comp K N-Locally Comp J × t K N-Locally Comp
38 4 5 37 syl2anc φ J × t K N-Locally Comp
39 27 mpompt w J × t K Cn L × X × Y 1 st 1 st w = z J × t K Cn L × X , y Y 1 st z
40 8 adantr φ w J × t K Cn L × X × Y J × t K TopOn X × Y
41 35 adantr φ w J × t K Cn L × X × Y L TopOn L
42 xp1st w J × t K Cn L × X × Y 1 st w J × t K Cn L × X
43 42 adantl φ w J × t K Cn L × X × Y 1 st w J × t K Cn L × X
44 xp1st 1 st w J × t K Cn L × X 1 st 1 st w J × t K Cn L
45 43 44 syl φ w J × t K Cn L × X × Y 1 st 1 st w J × t K Cn L
46 cnf2 J × t K TopOn X × Y L TopOn L 1 st 1 st w J × t K Cn L 1 st 1 st w : X × Y L
47 40 41 45 46 syl3anc φ w J × t K Cn L × X × Y 1 st 1 st w : X × Y L
48 47 feqmptd φ w J × t K Cn L × X × Y 1 st 1 st w = u X × Y 1 st 1 st w u
49 48 mpteq2dva φ w J × t K Cn L × X × Y 1 st 1 st w = w J × t K Cn L × X × Y u X × Y 1 st 1 st w u
50 39 49 eqtr3id φ z J × t K Cn L × X , y Y 1 st z = w J × t K Cn L × X × Y u X × Y 1 st 1 st w u
51 23 2 cnmpt1st φ z J × t K Cn L × X , y Y z L ^ ko J × t K × t J × t K Cn L ^ ko J × t K × t J
52 fveq2 t = z 1 st t = 1 st z
53 52 cbvmptv t J × t K Cn L × X 1 st t = z J × t K Cn L × X 1 st z
54 16 mpompt z J × t K Cn L × X 1 st z = f J × t K Cn L , x X f
55 13 1 cnmpt1st φ f J × t K Cn L , x X f L ^ ko J × t K × t J Cn L ^ ko J × t K
56 54 55 eqeltrid φ z J × t K Cn L × X 1 st z L ^ ko J × t K × t J Cn L ^ ko J × t K
57 53 56 eqeltrid φ t J × t K Cn L × X 1 st t L ^ ko J × t K × t J Cn L ^ ko J × t K
58 23 2 51 23 57 52 cnmpt21 φ z J × t K Cn L × X , y Y 1 st z L ^ ko J × t K × t J × t K Cn L ^ ko J × t K
59 50 58 eqeltrrd φ w J × t K Cn L × X × Y u X × Y 1 st 1 st w u L ^ ko J × t K × t J × t K Cn L ^ ko J × t K
60 28 mpompt w J × t K Cn L × X × Y 2 nd 1 st w = z J × t K Cn L × X , y Y 2 nd z
61 fveq2 t = z 2 nd t = 2 nd z
62 61 cbvmptv t J × t K Cn L × X 2 nd t = z J × t K Cn L × X 2 nd z
63 17 mpompt z J × t K Cn L × X 2 nd z = f J × t K Cn L , x X x
64 13 1 cnmpt2nd φ f J × t K Cn L , x X x L ^ ko J × t K × t J Cn J
65 63 64 eqeltrid φ z J × t K Cn L × X 2 nd z L ^ ko J × t K × t J Cn J
66 62 65 eqeltrid φ t J × t K Cn L × X 2 nd t L ^ ko J × t K × t J Cn J
67 23 2 51 23 66 61 cnmpt21 φ z J × t K Cn L × X , y Y 2 nd z L ^ ko J × t K × t J × t K Cn J
68 60 67 eqeltrid φ w J × t K Cn L × X × Y 2 nd 1 st w L ^ ko J × t K × t J × t K Cn J
69 29 mpompt w J × t K Cn L × X × Y 2 nd w = z J × t K Cn L × X , y Y y
70 23 2 cnmpt2nd φ z J × t K Cn L × X , y Y y L ^ ko J × t K × t J × t K Cn K
71 69 70 eqeltrid φ w J × t K Cn L × X × Y 2 nd w L ^ ko J × t K × t J × t K Cn K
72 33 68 71 cnmpt1t φ w J × t K Cn L × X × Y 2 nd 1 st w 2 nd w L ^ ko J × t K × t J × t K Cn J × t K
73 fveq2 u = 2 nd 1 st w 2 nd w 1 st 1 st w u = 1 st 1 st w 2 nd 1 st w 2 nd w
74 df-ov 2 nd 1 st w 1 st 1 st w 2 nd w = 1 st 1 st w 2 nd 1 st w 2 nd w
75 73 74 eqtr4di u = 2 nd 1 st w 2 nd w 1 st 1 st w u = 2 nd 1 st w 1 st 1 st w 2 nd w
76 33 8 35 38 59 72 75 cnmptk1p φ w J × t K Cn L × X × Y 2 nd 1 st w 1 st 1 st w 2 nd w L ^ ko J × t K × t J × t K Cn L
77 31 76 eqeltrrid φ z J × t K Cn L × X , y Y 2 nd z 1 st z y L ^ ko J × t K × t J × t K Cn L
78 23 2 77 cnmpt2k φ z J × t K Cn L × X y Y 2 nd z 1 st z y L ^ ko J × t K × t J Cn L ^ ko K
79 21 78 eqeltrrid φ f J × t K Cn L , x X y Y x f y L ^ ko J × t K × t J Cn L ^ ko K
80 13 1 79 cnmpt2k φ f J × t K Cn L x X y Y x f y L ^ ko J × t K Cn L ^ ko K ^ ko J
81 3 80 eqeltrid φ F L ^ ko J × t K Cn L ^ ko K ^ ko J
82 1 2 3 4 5 6 xkocnv φ F -1 = g J Cn L ^ ko K x X , y Y g x y
83 15 25 op1std z = x y 1 st z = x
84 83 fveq2d z = x y g 1 st z = g x
85 15 25 op2ndd z = x y 2 nd z = y
86 84 85 fveq12d z = x y g 1 st z 2 nd z = g x y
87 86 mpompt z X × Y g 1 st z 2 nd z = x X , y Y g x y
88 87 mpteq2i g J Cn L ^ ko K z X × Y g 1 st z 2 nd z = g J Cn L ^ ko K x X , y Y g x y
89 82 88 eqtr4di φ F -1 = g J Cn L ^ ko K z X × Y g 1 st z 2 nd z
90 nllytop J N-Locally Comp J Top
91 4 90 syl φ J Top
92 nllytop K N-Locally Comp K Top
93 5 92 syl φ K Top
94 xkotop K Top L Top L ^ ko K Top
95 93 6 94 syl2anc φ L ^ ko K Top
96 eqid L ^ ko K ^ ko J = L ^ ko K ^ ko J
97 96 xkotopon J Top L ^ ko K Top L ^ ko K ^ ko J TopOn J Cn L ^ ko K
98 91 95 97 syl2anc φ L ^ ko K ^ ko J TopOn J Cn L ^ ko K
99 vex g V
100 99 24 op1std w = g z 1 st w = g
101 99 24 op2ndd w = g z 2 nd w = z
102 101 fveq2d w = g z 1 st 2 nd w = 1 st z
103 100 102 fveq12d w = g z 1 st w 1 st 2 nd w = g 1 st z
104 101 fveq2d w = g z 2 nd 2 nd w = 2 nd z
105 103 104 fveq12d w = g z 1 st w 1 st 2 nd w 2 nd 2 nd w = g 1 st z 2 nd z
106 105 mpompt w J Cn L ^ ko K × X × Y 1 st w 1 st 2 nd w 2 nd 2 nd w = g J Cn L ^ ko K , z X × Y g 1 st z 2 nd z
107 txtopon L ^ ko K ^ ko J TopOn J Cn L ^ ko K J × t K TopOn X × Y L ^ ko K ^ ko J × t J × t K TopOn J Cn L ^ ko K × X × Y
108 98 8 107 syl2anc φ L ^ ko K ^ ko J × t J × t K TopOn J Cn L ^ ko K × X × Y
109 2 adantr φ w J Cn L ^ ko K × X × Y K TopOn Y
110 35 adantr φ w J Cn L ^ ko K × X × Y L TopOn L
111 eqid L ^ ko K = L ^ ko K
112 111 xkotopon K Top L Top L ^ ko K TopOn K Cn L
113 93 6 112 syl2anc φ L ^ ko K TopOn K Cn L
114 xp1st w J Cn L ^ ko K × X × Y 1 st w J Cn L ^ ko K
115 cnf2 J TopOn X L ^ ko K TopOn K Cn L 1 st w J Cn L ^ ko K 1 st w : X K Cn L
116 1 113 114 115 syl2an3an φ w J Cn L ^ ko K × X × Y 1 st w : X K Cn L
117 xp2nd w J Cn L ^ ko K × X × Y 2 nd w X × Y
118 117 adantl φ w J Cn L ^ ko K × X × Y 2 nd w X × Y
119 xp1st 2 nd w X × Y 1 st 2 nd w X
120 118 119 syl φ w J Cn L ^ ko K × X × Y 1 st 2 nd w X
121 116 120 ffvelrnd φ w J Cn L ^ ko K × X × Y 1 st w 1 st 2 nd w K Cn L
122 cnf2 K TopOn Y L TopOn L 1 st w 1 st 2 nd w K Cn L 1 st w 1 st 2 nd w : Y L
123 109 110 121 122 syl3anc φ w J Cn L ^ ko K × X × Y 1 st w 1 st 2 nd w : Y L
124 123 feqmptd φ w J Cn L ^ ko K × X × Y 1 st w 1 st 2 nd w = y Y 1 st w 1 st 2 nd w y
125 124 mpteq2dva φ w J Cn L ^ ko K × X × Y 1 st w 1 st 2 nd w = w J Cn L ^ ko K × X × Y y Y 1 st w 1 st 2 nd w y
126 100 mpompt w J Cn L ^ ko K × X × Y 1 st w = g J Cn L ^ ko K , z X × Y g
127 116 feqmptd φ w J Cn L ^ ko K × X × Y 1 st w = x X 1 st w x
128 127 mpteq2dva φ w J Cn L ^ ko K × X × Y 1 st w = w J Cn L ^ ko K × X × Y x X 1 st w x
129 126 128 eqtr3id φ g J Cn L ^ ko K , z X × Y g = w J Cn L ^ ko K × X × Y x X 1 st w x
130 98 8 cnmpt1st φ g J Cn L ^ ko K , z X × Y g L ^ ko K ^ ko J × t J × t K Cn L ^ ko K ^ ko J
131 129 130 eqeltrrd φ w J Cn L ^ ko K × X × Y x X 1 st w x L ^ ko K ^ ko J × t J × t K Cn L ^ ko K ^ ko J
132 102 mpompt w J Cn L ^ ko K × X × Y 1 st 2 nd w = g J Cn L ^ ko K , z X × Y 1 st z
133 98 8 cnmpt2nd φ g J Cn L ^ ko K , z X × Y z L ^ ko K ^ ko J × t J × t K Cn J × t K
134 52 cbvmptv t X × Y 1 st t = z X × Y 1 st z
135 83 mpompt z X × Y 1 st z = x X , y Y x
136 1 2 cnmpt1st φ x X , y Y x J × t K Cn J
137 135 136 eqeltrid φ z X × Y 1 st z J × t K Cn J
138 134 137 eqeltrid φ t X × Y 1 st t J × t K Cn J
139 98 8 133 8 138 52 cnmpt21 φ g J Cn L ^ ko K , z X × Y 1 st z L ^ ko K ^ ko J × t J × t K Cn J
140 132 139 eqeltrid φ w J Cn L ^ ko K × X × Y 1 st 2 nd w L ^ ko K ^ ko J × t J × t K Cn J
141 fveq2 x = 1 st 2 nd w 1 st w x = 1 st w 1 st 2 nd w
142 108 1 113 4 131 140 141 cnmptk1p φ w J Cn L ^ ko K × X × Y 1 st w 1 st 2 nd w L ^ ko K ^ ko J × t J × t K Cn L ^ ko K
143 125 142 eqeltrrd φ w J Cn L ^ ko K × X × Y y Y 1 st w 1 st 2 nd w y L ^ ko K ^ ko J × t J × t K Cn L ^ ko K
144 104 mpompt w J Cn L ^ ko K × X × Y 2 nd 2 nd w = g J Cn L ^ ko K , z X × Y 2 nd z
145 61 cbvmptv t X × Y 2 nd t = z X × Y 2 nd z
146 85 mpompt z X × Y 2 nd z = x X , y Y y
147 1 2 cnmpt2nd φ x X , y Y y J × t K Cn K
148 146 147 eqeltrid φ z X × Y 2 nd z J × t K Cn K
149 145 148 eqeltrid φ t X × Y 2 nd t J × t K Cn K
150 98 8 133 8 149 61 cnmpt21 φ g J Cn L ^ ko K , z X × Y 2 nd z L ^ ko K ^ ko J × t J × t K Cn K
151 144 150 eqeltrid φ w J Cn L ^ ko K × X × Y 2 nd 2 nd w L ^ ko K ^ ko J × t J × t K Cn K
152 fveq2 y = 2 nd 2 nd w 1 st w 1 st 2 nd w y = 1 st w 1 st 2 nd w 2 nd 2 nd w
153 108 2 35 5 143 151 152 cnmptk1p φ w J Cn L ^ ko K × X × Y 1 st w 1 st 2 nd w 2 nd 2 nd w L ^ ko K ^ ko J × t J × t K Cn L
154 106 153 eqeltrrid φ g J Cn L ^ ko K , z X × Y g 1 st z 2 nd z L ^ ko K ^ ko J × t J × t K Cn L
155 98 8 154 cnmpt2k φ g J Cn L ^ ko K z X × Y g 1 st z 2 nd z L ^ ko K ^ ko J Cn L ^ ko J × t K
156 89 155 eqeltrd φ F -1 L ^ ko K ^ ko J Cn L ^ ko J × t K
157 ishmeo F L ^ ko J × t K Homeo L ^ ko K ^ ko J F L ^ ko J × t K Cn L ^ ko K ^ ko J F -1 L ^ ko K ^ ko J Cn L ^ ko J × t K
158 81 156 157 sylanbrc φ F L ^ ko J × t K Homeo L ^ ko K ^ ko J