Metamath Proof Explorer


Theorem ptrest

Description: Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019)

Ref Expression
Hypotheses ptrest.0 φ A V
ptrest.1 φ F : A Top
ptrest.2 φ k A S W
Assertion ptrest φ 𝑡 F 𝑡 k A S = 𝑡 k A F k 𝑡 S

Proof

Step Hyp Ref Expression
1 ptrest.0 φ A V
2 ptrest.1 φ F : A Top
3 ptrest.2 φ k A S W
4 firest fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S = fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S
5 snex 𝑡 F V
6 fvex F u V
7 6 rgenw u A F u V
8 eqid u A , v F u w 𝑡 F w u -1 v = u A , v F u w 𝑡 F w u -1 v
9 8 mpoexxg A V u A F u V u A , v F u w 𝑡 F w u -1 v V
10 1 7 9 sylancl φ u A , v F u w 𝑡 F w u -1 v V
11 rnexg u A , v F u w 𝑡 F w u -1 v V ran u A , v F u w 𝑡 F w u -1 v V
12 10 11 syl φ ran u A , v F u w 𝑡 F w u -1 v V
13 unexg 𝑡 F V ran u A , v F u w 𝑡 F w u -1 v V 𝑡 F ran u A , v F u w 𝑡 F w u -1 v V
14 5 12 13 sylancr φ 𝑡 F ran u A , v F u w 𝑡 F w u -1 v V
15 3 ralrimiva φ k A S W
16 ixpexg k A S W k A S V
17 15 16 syl φ k A S V
18 restval 𝑡 F ran u A , v F u w 𝑡 F w u -1 v V k A S V 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S = ran x 𝑡 F ran u A , v F u w 𝑡 F w u -1 v x k A S
19 14 17 18 syl2anc φ 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S = ran x 𝑡 F ran u A , v F u w 𝑡 F w u -1 v x k A S
20 mptun x 𝑡 F ran u A , v F u w 𝑡 F w u -1 v x k A S = x 𝑡 F x k A S x ran u A , v F u w 𝑡 F w u -1 v x k A S
21 20 rneqi ran x 𝑡 F ran u A , v F u w 𝑡 F w u -1 v x k A S = ran x 𝑡 F x k A S x ran u A , v F u w 𝑡 F w u -1 v x k A S
22 rnun ran x 𝑡 F x k A S x ran u A , v F u w 𝑡 F w u -1 v x k A S = ran x 𝑡 F x k A S ran x ran u A , v F u w 𝑡 F w u -1 v x k A S
23 21 22 eqtri ran x 𝑡 F ran u A , v F u w 𝑡 F w u -1 v x k A S = ran x 𝑡 F x k A S ran x ran u A , v F u w 𝑡 F w u -1 v x k A S
24 elsni x 𝑡 F x = 𝑡 F
25 24 ineq1d x 𝑡 F x k A S = 𝑡 F k A S
26 25 mpteq2ia x 𝑡 F x k A S = x 𝑡 F 𝑡 F k A S
27 fvex 𝑡 F V
28 27 uniex 𝑡 F V
29 28 inex1 𝑡 F k A S V
30 fmptsn 𝑡 F V 𝑡 F k A S V 𝑡 F 𝑡 F k A S = x 𝑡 F 𝑡 F k A S
31 28 29 30 mp2an 𝑡 F 𝑡 F k A S = x 𝑡 F 𝑡 F k A S
32 26 31 eqtr4i x 𝑡 F x k A S = 𝑡 F 𝑡 F k A S
33 32 rneqi ran x 𝑡 F x k A S = ran 𝑡 F 𝑡 F k A S
34 28 rnsnop ran 𝑡 F 𝑡 F k A S = 𝑡 F k A S
35 33 34 eqtri ran x 𝑡 F x k A S = 𝑡 F k A S
36 2 ffvelrnda φ k A F k Top
37 inss1 F k S F k
38 eqid F k = F k
39 38 restuni F k Top F k S F k F k S = F k 𝑡 F k S
40 36 37 39 sylancl φ k A F k S = F k 𝑡 F k S
41 fvex F k V
42 38 restin F k V S W F k 𝑡 S = F k 𝑡 S F k
43 41 3 42 sylancr φ k A F k 𝑡 S = F k 𝑡 S F k
44 incom S F k = F k S
45 44 oveq2i F k 𝑡 S F k = F k 𝑡 F k S
46 43 45 eqtrdi φ k A F k 𝑡 S = F k 𝑡 F k S
47 46 unieqd φ k A F k 𝑡 S = F k 𝑡 F k S
48 40 47 eqtr4d φ k A F k S = F k 𝑡 S
49 48 ixpeq2dva φ k A F k S = k A F k 𝑡 S
50 ixpin k A F k S = k A F k k A S
51 nfcv _ y F k 𝑡 S
52 nfcv _ k F y
53 nfcv _ k 𝑡
54 nfcsb1v _ k y / k S
55 52 53 54 nfov _ k F y 𝑡 y / k S
56 55 nfuni _ k F y 𝑡 y / k S
57 fveq2 k = y F k = F y
58 csbeq1a k = y S = y / k S
59 57 58 oveq12d k = y F k 𝑡 S = F y 𝑡 y / k S
60 59 unieqd k = y F k 𝑡 S = F y 𝑡 y / k S
61 51 56 60 cbvixp k A F k 𝑡 S = y A F y 𝑡 y / k S
62 ixpeq2 y A k A F k 𝑡 S y = F y 𝑡 y / k S y A k A F k 𝑡 S y = y A F y 𝑡 y / k S
63 ovex F y 𝑡 y / k S V
64 nfcv _ k y
65 eqid k A F k 𝑡 S = k A F k 𝑡 S
66 64 55 59 65 fvmptf y A F y 𝑡 y / k S V k A F k 𝑡 S y = F y 𝑡 y / k S
67 63 66 mpan2 y A k A F k 𝑡 S y = F y 𝑡 y / k S
68 67 unieqd y A k A F k 𝑡 S y = F y 𝑡 y / k S
69 62 68 mprg y A k A F k 𝑡 S y = y A F y 𝑡 y / k S
70 61 69 eqtr4i k A F k 𝑡 S = y A k A F k 𝑡 S y
71 49 50 70 3eqtr3g φ k A F k k A S = y A k A F k 𝑡 S y
72 eqid 𝑡 F = 𝑡 F
73 72 ptuni A V F : A Top k A F k = 𝑡 F
74 1 2 73 syl2anc φ k A F k = 𝑡 F
75 74 ineq1d φ k A F k k A S = 𝑡 F k A S
76 resttop F k Top S W F k 𝑡 S Top
77 36 3 76 syl2anc φ k A F k 𝑡 S Top
78 77 fmpttd φ k A F k 𝑡 S : A Top
79 eqid 𝑡 k A F k 𝑡 S = 𝑡 k A F k 𝑡 S
80 79 ptuni A V k A F k 𝑡 S : A Top y A k A F k 𝑡 S y = 𝑡 k A F k 𝑡 S
81 1 78 80 syl2anc φ y A k A F k 𝑡 S y = 𝑡 k A F k 𝑡 S
82 71 75 81 3eqtr3d φ 𝑡 F k A S = 𝑡 k A F k 𝑡 S
83 82 sneqd φ 𝑡 F k A S = 𝑡 k A F k 𝑡 S
84 35 83 syl5eq φ ran x 𝑡 F x k A S = 𝑡 k A F k 𝑡 S
85 vex w V
86 85 elixp w k A S w Fn A k A w k S
87 86 simprbi w k A S k A w k S
88 nfcsb1v _ k u / k S
89 88 nfel2 k w u u / k S
90 fveq2 k = u w k = w u
91 csbeq1a k = u S = u / k S
92 90 91 eleq12d k = u w k S w u u / k S
93 89 92 rspc u A k A w k S w u u / k S
94 87 93 syl5 u A w k A S w u u / k S
95 94 pm4.71d u A w k A S w k A S w u u / k S
96 95 anbi2d u A w 𝑡 F w u v w k A S w 𝑡 F w u v w k A S w u u / k S
97 an4 w 𝑡 F w u v w k A S w u u / k S w 𝑡 F w k A S w u v w u u / k S
98 elin w u v u / k S w u v w u u / k S
99 98 anbi2i w 𝑡 F w k A S w u v u / k S w 𝑡 F w k A S w u v w u u / k S
100 97 99 bitr4i w 𝑡 F w u v w k A S w u u / k S w 𝑡 F w k A S w u v u / k S
101 96 100 bitrdi u A w 𝑡 F w u v w k A S w 𝑡 F w k A S w u v u / k S
102 elin w 𝑡 F k A S w 𝑡 F w k A S
103 82 eleq2d φ w 𝑡 F k A S w 𝑡 k A F k 𝑡 S
104 102 103 bitr3id φ w 𝑡 F w k A S w 𝑡 k A F k 𝑡 S
105 104 anbi1d φ w 𝑡 F w k A S w u v u / k S w 𝑡 k A F k 𝑡 S w u v u / k S
106 101 105 sylan9bbr φ u A w 𝑡 F w u v w k A S w 𝑡 k A F k 𝑡 S w u v u / k S
107 106 abbidv φ u A w | w 𝑡 F w u v w k A S = w | w 𝑡 k A F k 𝑡 S w u v u / k S
108 eqid w 𝑡 F w u = w 𝑡 F w u
109 108 mptpreima w 𝑡 F w u -1 v = w 𝑡 F | w u v
110 df-rab w 𝑡 F | w u v = w | w 𝑡 F w u v
111 109 110 eqtr2i w | w 𝑡 F w u v = w 𝑡 F w u -1 v
112 abid2 w | w k A S = k A S
113 111 112 ineq12i w | w 𝑡 F w u v w | w k A S = w 𝑡 F w u -1 v k A S
114 inab w | w 𝑡 F w u v w | w k A S = w | w 𝑡 F w u v w k A S
115 113 114 eqtr3i w 𝑡 F w u -1 v k A S = w | w 𝑡 F w u v w k A S
116 eqid w 𝑡 k A F k 𝑡 S w u = w 𝑡 k A F k 𝑡 S w u
117 116 mptpreima w 𝑡 k A F k 𝑡 S w u -1 v u / k S = w 𝑡 k A F k 𝑡 S | w u v u / k S
118 df-rab w 𝑡 k A F k 𝑡 S | w u v u / k S = w | w 𝑡 k A F k 𝑡 S w u v u / k S
119 117 118 eqtri w 𝑡 k A F k 𝑡 S w u -1 v u / k S = w | w 𝑡 k A F k 𝑡 S w u v u / k S
120 107 115 119 3eqtr4g φ u A w 𝑡 F w u -1 v k A S = w 𝑡 k A F k 𝑡 S w u -1 v u / k S
121 120 eqeq2d φ u A x = w 𝑡 F w u -1 v k A S x = w 𝑡 k A F k 𝑡 S w u -1 v u / k S
122 121 rexbidv φ u A v F u x = w 𝑡 F w u -1 v k A S v F u x = w 𝑡 k A F k 𝑡 S w u -1 v u / k S
123 ineq1 v = y v u / k S = y u / k S
124 123 imaeq2d v = y w 𝑡 k A F k 𝑡 S w u -1 v u / k S = w 𝑡 k A F k 𝑡 S w u -1 y u / k S
125 124 eqeq2d v = y x = w 𝑡 k A F k 𝑡 S w u -1 v u / k S x = w 𝑡 k A F k 𝑡 S w u -1 y u / k S
126 125 cbvrexvw v F u x = w 𝑡 k A F k 𝑡 S w u -1 v u / k S y F u x = w 𝑡 k A F k 𝑡 S w u -1 y u / k S
127 122 126 bitrdi φ u A v F u x = w 𝑡 F w u -1 v k A S y F u x = w 𝑡 k A F k 𝑡 S w u -1 y u / k S
128 vex y V
129 128 inex1 y u / k S V
130 129 a1i φ u A y F u y u / k S V
131 ovex F u 𝑡 u / k S V
132 nfcv _ k u
133 nfcv _ k F u
134 133 53 88 nfov _ k F u 𝑡 u / k S
135 fveq2 k = u F k = F u
136 135 91 oveq12d k = u F k 𝑡 S = F u 𝑡 u / k S
137 132 134 136 65 fvmptf u A F u 𝑡 u / k S V k A F k 𝑡 S u = F u 𝑡 u / k S
138 131 137 mpan2 u A k A F k 𝑡 S u = F u 𝑡 u / k S
139 138 adantl φ u A k A F k 𝑡 S u = F u 𝑡 u / k S
140 139 eleq2d φ u A v k A F k 𝑡 S u v F u 𝑡 u / k S
141 nfv k φ u A
142 nfcsb1v _ k u / k W
143 88 142 nfel k u / k S u / k W
144 141 143 nfim k φ u A u / k S u / k W
145 eleq1w k = u k A u A
146 145 anbi2d k = u φ k A φ u A
147 csbeq1a k = u W = u / k W
148 91 147 eleq12d k = u S W u / k S u / k W
149 146 148 imbi12d k = u φ k A S W φ u A u / k S u / k W
150 144 149 3 chvarfv φ u A u / k S u / k W
151 elrest F u V u / k S u / k W v F u 𝑡 u / k S y F u v = y u / k S
152 6 150 151 sylancr φ u A v F u 𝑡 u / k S y F u v = y u / k S
153 140 152 bitrd φ u A v k A F k 𝑡 S u y F u v = y u / k S
154 imaeq2 v = y u / k S w 𝑡 k A F k 𝑡 S w u -1 v = w 𝑡 k A F k 𝑡 S w u -1 y u / k S
155 154 eqeq2d v = y u / k S x = w 𝑡 k A F k 𝑡 S w u -1 v x = w 𝑡 k A F k 𝑡 S w u -1 y u / k S
156 155 adantl φ u A v = y u / k S x = w 𝑡 k A F k 𝑡 S w u -1 v x = w 𝑡 k A F k 𝑡 S w u -1 y u / k S
157 130 153 156 rexxfr2d φ u A v k A F k 𝑡 S u x = w 𝑡 k A F k 𝑡 S w u -1 v y F u x = w 𝑡 k A F k 𝑡 S w u -1 y u / k S
158 127 157 bitr4d φ u A v F u x = w 𝑡 F w u -1 v k A S v k A F k 𝑡 S u x = w 𝑡 k A F k 𝑡 S w u -1 v
159 158 rexbidva φ u A v F u x = w 𝑡 F w u -1 v k A S u A v k A F k 𝑡 S u x = w 𝑡 k A F k 𝑡 S w u -1 v
160 159 abbidv φ x | u A v F u x = w 𝑡 F w u -1 v k A S = x | u A v k A F k 𝑡 S u x = w 𝑡 k A F k 𝑡 S w u -1 v
161 eqid x ran u A , v F u w 𝑡 F w u -1 v x k A S = x ran u A , v F u w 𝑡 F w u -1 v x k A S
162 161 rnmpt ran x ran u A , v F u w 𝑡 F w u -1 v x k A S = y | x ran u A , v F u w 𝑡 F w u -1 v y = x k A S
163 nfre1 x x ran u A , v F u w 𝑡 F w u -1 v y = x k A S
164 nfv y u A v F u x = w 𝑡 F w u -1 v k A S
165 28 mptex w 𝑡 F w u V
166 165 cnvex w 𝑡 F w u -1 V
167 166 imaex w 𝑡 F w u -1 v V
168 167 rgen2w u A v F u w 𝑡 F w u -1 v V
169 ineq1 x = w 𝑡 F w u -1 v x k A S = w 𝑡 F w u -1 v k A S
170 169 eqeq2d x = w 𝑡 F w u -1 v y = x k A S y = w 𝑡 F w u -1 v k A S
171 8 170 rexrnmpo u A v F u w 𝑡 F w u -1 v V x ran u A , v F u w 𝑡 F w u -1 v y = x k A S u A v F u y = w 𝑡 F w u -1 v k A S
172 168 171 ax-mp x ran u A , v F u w 𝑡 F w u -1 v y = x k A S u A v F u y = w 𝑡 F w u -1 v k A S
173 eqeq1 y = x y = w 𝑡 F w u -1 v k A S x = w 𝑡 F w u -1 v k A S
174 173 2rexbidv y = x u A v F u y = w 𝑡 F w u -1 v k A S u A v F u x = w 𝑡 F w u -1 v k A S
175 172 174 syl5bb y = x x ran u A , v F u w 𝑡 F w u -1 v y = x k A S u A v F u x = w 𝑡 F w u -1 v k A S
176 163 164 175 cbvabw y | x ran u A , v F u w 𝑡 F w u -1 v y = x k A S = x | u A v F u x = w 𝑡 F w u -1 v k A S
177 162 176 eqtri ran x ran u A , v F u w 𝑡 F w u -1 v x k A S = x | u A v F u x = w 𝑡 F w u -1 v k A S
178 eqid u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v = u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
179 178 rnmpo ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v = x | u A v k A F k 𝑡 S u x = w 𝑡 k A F k 𝑡 S w u -1 v
180 160 177 179 3eqtr4g φ ran x ran u A , v F u w 𝑡 F w u -1 v x k A S = ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
181 84 180 uneq12d φ ran x 𝑡 F x k A S ran x ran u A , v F u w 𝑡 F w u -1 v x k A S = 𝑡 k A F k 𝑡 S ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
182 23 181 syl5eq φ ran x 𝑡 F ran u A , v F u w 𝑡 F w u -1 v x k A S = 𝑡 k A F k 𝑡 S ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
183 19 182 eqtrd φ 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S = 𝑡 k A F k 𝑡 S ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
184 183 fveq2d φ fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S = fi 𝑡 k A F k 𝑡 S ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
185 4 184 eqtr3id φ fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S = fi 𝑡 k A F k 𝑡 S ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
186 185 fveq2d φ topGen fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S = topGen fi 𝑡 k A F k 𝑡 S ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
187 eqid 𝑡 F = 𝑡 F
188 72 187 8 ptval2 A V F : A Top 𝑡 F = topGen fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v
189 1 2 188 syl2anc φ 𝑡 F = topGen fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v
190 189 oveq1d φ 𝑡 F 𝑡 k A S = topGen fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S
191 fvex fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v V
192 tgrest fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v V k A S V topGen fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S = topGen fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S
193 191 17 192 sylancr φ topGen fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S = topGen fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S
194 190 193 eqtr4d φ 𝑡 F 𝑡 k A S = topGen fi 𝑡 F ran u A , v F u w 𝑡 F w u -1 v 𝑡 k A S
195 eqid 𝑡 k A F k 𝑡 S = 𝑡 k A F k 𝑡 S
196 79 195 178 ptval2 A V k A F k 𝑡 S : A Top 𝑡 k A F k 𝑡 S = topGen fi 𝑡 k A F k 𝑡 S ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
197 1 78 196 syl2anc φ 𝑡 k A F k 𝑡 S = topGen fi 𝑡 k A F k 𝑡 S ran u A , v k A F k 𝑡 S u w 𝑡 k A F k 𝑡 S w u -1 v
198 186 194 197 3eqtr4d φ 𝑡 F 𝑡 k A S = 𝑡 k A F k 𝑡 S