Metamath Proof Explorer


Theorem txrest

Description: The subspace of a topological product space induced by a subset with a Cartesian product representation is a topological product of the subspaces induced by the subspaces of the terms of the products. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion txrest R V S W A X B Y R × t S 𝑡 A × B = R 𝑡 A × t S 𝑡 B

Proof

Step Hyp Ref Expression
1 eqid ran r R , s S r × s = ran r R , s S r × s
2 1 txval R V S W R × t S = topGen ran r R , s S r × s
3 2 adantr R V S W A X B Y R × t S = topGen ran r R , s S r × s
4 3 oveq1d R V S W A X B Y R × t S 𝑡 A × B = topGen ran r R , s S r × s 𝑡 A × B
5 1 txbasex R V S W ran r R , s S r × s V
6 xpexg A X B Y A × B V
7 tgrest ran r R , s S r × s V A × B V topGen ran r R , s S r × s 𝑡 A × B = topGen ran r R , s S r × s 𝑡 A × B
8 5 6 7 syl2an R V S W A X B Y topGen ran r R , s S r × s 𝑡 A × B = topGen ran r R , s S r × s 𝑡 A × B
9 elrest ran r R , s S r × s V A × B V x ran r R , s S r × s 𝑡 A × B w ran r R , s S r × s x = w A × B
10 5 6 9 syl2an R V S W A X B Y x ran r R , s S r × s 𝑡 A × B w ran r R , s S r × s x = w A × B
11 vex r V
12 11 inex1 r A V
13 12 a1i R V S W A X B Y r R r A V
14 elrest R V A X u R 𝑡 A r R u = r A
15 14 ad2ant2r R V S W A X B Y u R 𝑡 A r R u = r A
16 xpeq1 u = r A u × v = r A × v
17 16 eqeq2d u = r A x = u × v x = r A × v
18 17 rexbidv u = r A v S 𝑡 B x = u × v v S 𝑡 B x = r A × v
19 vex s V
20 19 inex1 s B V
21 20 a1i R V S W A X B Y s S s B V
22 elrest S W B Y v S 𝑡 B s S v = s B
23 22 ad2ant2l R V S W A X B Y v S 𝑡 B s S v = s B
24 xpeq2 v = s B r A × v = r A × s B
25 24 eqeq2d v = s B x = r A × v x = r A × s B
26 25 adantl R V S W A X B Y v = s B x = r A × v x = r A × s B
27 21 23 26 rexxfr2d R V S W A X B Y v S 𝑡 B x = r A × v s S x = r A × s B
28 18 27 sylan9bbr R V S W A X B Y u = r A v S 𝑡 B x = u × v s S x = r A × s B
29 13 15 28 rexxfr2d R V S W A X B Y u R 𝑡 A v S 𝑡 B x = u × v r R s S x = r A × s B
30 11 19 xpex r × s V
31 30 rgen2w r R s S r × s V
32 eqid r R , s S r × s = r R , s S r × s
33 ineq1 w = r × s w A × B = r × s A × B
34 inxp r × s A × B = r A × s B
35 33 34 eqtrdi w = r × s w A × B = r A × s B
36 35 eqeq2d w = r × s x = w A × B x = r A × s B
37 32 36 rexrnmpo r R s S r × s V w ran r R , s S r × s x = w A × B r R s S x = r A × s B
38 31 37 ax-mp w ran r R , s S r × s x = w A × B r R s S x = r A × s B
39 29 38 bitr4di R V S W A X B Y u R 𝑡 A v S 𝑡 B x = u × v w ran r R , s S r × s x = w A × B
40 10 39 bitr4d R V S W A X B Y x ran r R , s S r × s 𝑡 A × B u R 𝑡 A v S 𝑡 B x = u × v
41 40 abbi2dv R V S W A X B Y ran r R , s S r × s 𝑡 A × B = x | u R 𝑡 A v S 𝑡 B x = u × v
42 eqid u R 𝑡 A , v S 𝑡 B u × v = u R 𝑡 A , v S 𝑡 B u × v
43 42 rnmpo ran u R 𝑡 A , v S 𝑡 B u × v = x | u R 𝑡 A v S 𝑡 B x = u × v
44 41 43 eqtr4di R V S W A X B Y ran r R , s S r × s 𝑡 A × B = ran u R 𝑡 A , v S 𝑡 B u × v
45 44 fveq2d R V S W A X B Y topGen ran r R , s S r × s 𝑡 A × B = topGen ran u R 𝑡 A , v S 𝑡 B u × v
46 4 8 45 3eqtr2d R V S W A X B Y R × t S 𝑡 A × B = topGen ran u R 𝑡 A , v S 𝑡 B u × v
47 ovex R 𝑡 A V
48 ovex S 𝑡 B V
49 eqid ran u R 𝑡 A , v S 𝑡 B u × v = ran u R 𝑡 A , v S 𝑡 B u × v
50 49 txval R 𝑡 A V S 𝑡 B V R 𝑡 A × t S 𝑡 B = topGen ran u R 𝑡 A , v S 𝑡 B u × v
51 47 48 50 mp2an R 𝑡 A × t S 𝑡 B = topGen ran u R 𝑡 A , v S 𝑡 B u × v
52 46 51 eqtr4di R V S W A X B Y R × t S 𝑡 A × B = R 𝑡 A × t S 𝑡 B