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 = J
txhmeo.2 Y = K
txhmeo.3 φ F J Homeo L
txhmeo.4 φ G K Homeo M
Assertion txhmeo φ x X , y Y F x G y J × t K Homeo L × t M

Proof

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