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 e. V /\ S e. W ) /\ ( A e. X /\ B e. Y ) ) -> ( ( R tX S ) |`t ( A X. B ) ) = ( ( R |`t A ) tX ( S |`t B ) ) )

Proof

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