Metamath Proof Explorer

Theorem txhmeo

Description: Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses txhmeo.1 
|- X = U. J
txhmeo.2 
|- Y = U. K
txhmeo.3 
|- ( ph -> F e. ( J Homeo L ) )
txhmeo.4 
|- ( ph -> G e. ( K Homeo M ) )
Assertion txhmeo 
|- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) )

Proof

Step Hyp Ref Expression
1 txhmeo.1 
 |-  X = U. J
2 txhmeo.2 
 |-  Y = U. K
3 txhmeo.3 
 |-  ( ph -> F e. ( J Homeo L ) )
4 txhmeo.4 
 |-  ( ph -> G e. ( K Homeo M ) )
5 hmeocn 
 |-  ( F e. ( J Homeo L ) -> F e. ( J Cn L ) )
6 3 5 syl 
 |-  ( ph -> F e. ( J Cn L ) )
7 cntop1 
 |-  ( F e. ( J Cn L ) -> J e. Top )
8 6 7 syl 
 |-  ( ph -> J e. Top )
9 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
10 8 9 sylib 
 |-  ( ph -> J e. ( TopOn ` X ) )
11 hmeocn 
 |-  ( G e. ( K Homeo M ) -> G e. ( K Cn M ) )
12 4 11 syl 
 |-  ( ph -> G e. ( K Cn M ) )
13 cntop1 
 |-  ( G e. ( K Cn M ) -> K e. Top )
14 12 13 syl 
 |-  ( ph -> K e. Top )
15 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
16 14 15 sylib 
 |-  ( ph -> K e. ( TopOn ` Y ) )
17 10 16 cnmpt1st 
 |-  ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )
18 10 16 17 6 cnmpt21f 
 |-  ( ph -> ( x e. X , y e. Y |-> ( F ` x ) ) e. ( ( J tX K ) Cn L ) )
19 10 16 cnmpt2nd 
 |-  ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )
20 10 16 19 12 cnmpt21f 
 |-  ( ph -> ( x e. X , y e. Y |-> ( G ` y ) ) e. ( ( J tX K ) Cn M ) )
21 10 16 18 20 cnmpt2t 
 |-  ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
22 vex 
 |-  x e. _V
23 vex 
 |-  y e. _V
24 22 23 op1std 
 |-  ( u = <. x , y >. -> ( 1st ` u ) = x )
25 24 fveq2d 
 |-  ( u = <. x , y >. -> ( F ` ( 1st ` u ) ) = ( F ` x ) )
26 22 23 op2ndd 
 |-  ( u = <. x , y >. -> ( 2nd ` u ) = y )
27 26 fveq2d 
 |-  ( u = <. x , y >. -> ( G ` ( 2nd ` u ) ) = ( G ` y ) )
28 25 27 opeq12d 
 |-  ( u = <. x , y >. -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. = <. ( F ` x ) , ( G ` y ) >. )
29 28 mpompt 
 |-  ( u e. ( X X. Y ) |-> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. ) = ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. )
30 29 eqcomi 
 |-  ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( u e. ( X X. Y ) |-> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. )
31 eqid 
 |-  U. L = U. L
32 1 31 cnf 
 |-  ( F e. ( J Cn L ) -> F : X --> U. L )
33 6 32 syl 
 |-  ( ph -> F : X --> U. L )
34 xp1st 
 |-  ( u e. ( X X. Y ) -> ( 1st ` u ) e. X )
35 ffvelrn 
 |-  ( ( F : X --> U. L /\ ( 1st ` u ) e. X ) -> ( F ` ( 1st ` u ) ) e. U. L )
36 33 34 35 syl2an 
 |-  ( ( ph /\ u e. ( X X. Y ) ) -> ( F ` ( 1st ` u ) ) e. U. L )
37 eqid 
 |-  U. M = U. M
38 2 37 cnf 
 |-  ( G e. ( K Cn M ) -> G : Y --> U. M )
39 12 38 syl 
 |-  ( ph -> G : Y --> U. M )
40 xp2nd 
 |-  ( u e. ( X X. Y ) -> ( 2nd ` u ) e. Y )
41 ffvelrn 
 |-  ( ( G : Y --> U. M /\ ( 2nd ` u ) e. Y ) -> ( G ` ( 2nd ` u ) ) e. U. M )
42 39 40 41 syl2an 
 |-  ( ( ph /\ u e. ( X X. Y ) ) -> ( G ` ( 2nd ` u ) ) e. U. M )
43 36 42 opelxpd 
 |-  ( ( ph /\ u e. ( X X. Y ) ) -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. e. ( U. L X. U. M ) )
44 1 31 hmeof1o 
 |-  ( F e. ( J Homeo L ) -> F : X -1-1-onto-> U. L )
45 3 44 syl 
 |-  ( ph -> F : X -1-1-onto-> U. L )
46 f1ocnv 
 |-  ( F : X -1-1-onto-> U. L -> `' F : U. L -1-1-onto-> X )
47 f1of 
 |-  ( `' F : U. L -1-1-onto-> X -> `' F : U. L --> X )
48 45 46 47 3syl 
 |-  ( ph -> `' F : U. L --> X )
49 xp1st 
 |-  ( v e. ( U. L X. U. M ) -> ( 1st ` v ) e. U. L )
50 ffvelrn 
 |-  ( ( `' F : U. L --> X /\ ( 1st ` v ) e. U. L ) -> ( `' F ` ( 1st ` v ) ) e. X )
51 48 49 50 syl2an 
 |-  ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' F ` ( 1st ` v ) ) e. X )
52 2 37 hmeof1o 
 |-  ( G e. ( K Homeo M ) -> G : Y -1-1-onto-> U. M )
53 4 52 syl 
 |-  ( ph -> G : Y -1-1-onto-> U. M )
54 f1ocnv 
 |-  ( G : Y -1-1-onto-> U. M -> `' G : U. M -1-1-onto-> Y )
55 f1of 
 |-  ( `' G : U. M -1-1-onto-> Y -> `' G : U. M --> Y )
56 53 54 55 3syl 
 |-  ( ph -> `' G : U. M --> Y )
57 xp2nd 
 |-  ( v e. ( U. L X. U. M ) -> ( 2nd ` v ) e. U. M )
58 ffvelrn 
 |-  ( ( `' G : U. M --> Y /\ ( 2nd ` v ) e. U. M ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
59 56 57 58 syl2an 
 |-  ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
60 51 59 opelxpd 
 |-  ( ( ph /\ v e. ( U. L X. U. M ) ) -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. e. ( X X. Y ) )
61 45 adantr 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> F : X -1-1-onto-> U. L )
62 34 ad2antrl 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` u ) e. X )
63 49 ad2antll 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` v ) e. U. L )
64 f1ocnvfvb 
 |-  ( ( F : X -1-1-onto-> U. L /\ ( 1st ` u ) e. X /\ ( 1st ` v ) e. U. L ) -> ( ( F ` ( 1st ` u ) ) = ( 1st ` v ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) ) )
65 61 62 63 64 syl3anc 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( F ` ( 1st ` u ) ) = ( 1st ` v ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) ) )
66 eqcom 
 |-  ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( F ` ( 1st ` u ) ) = ( 1st ` v ) )
67 eqcom 
 |-  ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) )
68 65 66 67 3bitr4g 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) ) )
69 53 adantr 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> G : Y -1-1-onto-> U. M )
70 40 ad2antrl 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` u ) e. Y )
71 57 ad2antll 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` v ) e. U. M )
72 f1ocnvfvb 
 |-  ( ( G : Y -1-1-onto-> U. M /\ ( 2nd ` u ) e. Y /\ ( 2nd ` v ) e. U. M ) -> ( ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) ) )
73 69 70 71 72 syl3anc 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) ) )
74 eqcom 
 |-  ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) )
75 eqcom 
 |-  ( ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) )
76 73 74 75 3bitr4g 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) )
77 68 76 anbi12d 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) /\ ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) ) <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )
78 eqop 
 |-  ( v e. ( U. L X. U. M ) -> ( v = <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. <-> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) /\ ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) ) ) )
79 78 ad2antll 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( v = <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. <-> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) /\ ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) ) ) )
80 eqop 
 |-  ( u e. ( X X. Y ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )
81 80 ad2antrl 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )
82 77 79 81 3bitr4rd 
 |-  ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> v = <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. ) )
83 30 43 60 82 f1ocnv2d 
 |-  ( ph -> ( ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) : ( X X. Y ) -1-1-onto-> ( U. L X. U. M ) /\ `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( v e. ( U. L X. U. M ) |-> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. ) ) )
84 83 simprd 
 |-  ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( v e. ( U. L X. U. M ) |-> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. ) )
85 vex 
 |-  z e. _V
86 vex 
 |-  w e. _V
87 85 86 op1std 
 |-  ( v = <. z , w >. -> ( 1st ` v ) = z )
88 87 fveq2d 
 |-  ( v = <. z , w >. -> ( `' F ` ( 1st ` v ) ) = ( `' F ` z ) )
89 85 86 op2ndd 
 |-  ( v = <. z , w >. -> ( 2nd ` v ) = w )
90 89 fveq2d 
 |-  ( v = <. z , w >. -> ( `' G ` ( 2nd ` v ) ) = ( `' G ` w ) )
91 88 90 opeq12d 
 |-  ( v = <. z , w >. -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. = <. ( `' F ` z ) , ( `' G ` w ) >. )
92 91 mpompt 
 |-  ( v e. ( U. L X. U. M ) |-> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. ) = ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. )
93 84 92 eqtrdi 
 |-  ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. ) )
94 cntop2 
 |-  ( F e. ( J Cn L ) -> L e. Top )
95 6 94 syl 
 |-  ( ph -> L e. Top )
96 31 toptopon 
 |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
97 95 96 sylib 
 |-  ( ph -> L e. ( TopOn ` U. L ) )
98 cntop2 
 |-  ( G e. ( K Cn M ) -> M e. Top )
99 12 98 syl 
 |-  ( ph -> M e. Top )
100 37 toptopon 
 |-  ( M e. Top <-> M e. ( TopOn ` U. M ) )
101 99 100 sylib 
 |-  ( ph -> M e. ( TopOn ` U. M ) )
102 97 101 cnmpt1st 
 |-  ( ph -> ( z e. U. L , w e. U. M |-> z ) e. ( ( L tX M ) Cn L ) )
103 hmeocnvcn 
 |-  ( F e. ( J Homeo L ) -> `' F e. ( L Cn J ) )
104 3 103 syl 
 |-  ( ph -> `' F e. ( L Cn J ) )
105 97 101 102 104 cnmpt21f 
 |-  ( ph -> ( z e. U. L , w e. U. M |-> ( `' F ` z ) ) e. ( ( L tX M ) Cn J ) )
106 97 101 cnmpt2nd 
 |-  ( ph -> ( z e. U. L , w e. U. M |-> w ) e. ( ( L tX M ) Cn M ) )
107 hmeocnvcn 
 |-  ( G e. ( K Homeo M ) -> `' G e. ( M Cn K ) )
108 4 107 syl 
 |-  ( ph -> `' G e. ( M Cn K ) )
109 97 101 106 108 cnmpt21f 
 |-  ( ph -> ( z e. U. L , w e. U. M |-> ( `' G ` w ) ) e. ( ( L tX M ) Cn K ) )
110 97 101 105 109 cnmpt2t 
 |-  ( ph -> ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )
111 93 110 eqeltrd 
 |-  ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )
112 ishmeo 
 |-  ( ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) <-> ( ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) /\ `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) ) )
113 21 111 112 sylanbrc 
 |-  ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) )