Metamath Proof Explorer


Theorem pt1hmeo

Description: The canonical homeomorphism from a topological product on a singleton to the topology of the factor. (Contributed by Mario Carneiro, 3-Feb-2015) (Proof shortened by AV, 18-Apr-2021)

Ref Expression
Hypotheses pt1hmeo.j K = 𝑡 A J
pt1hmeo.a φ A V
pt1hmeo.r φ J TopOn X
Assertion pt1hmeo φ x X A x J Homeo K

Proof

Step Hyp Ref Expression
1 pt1hmeo.j K = 𝑡 A J
2 pt1hmeo.a φ A V
3 pt1hmeo.r φ J TopOn X
4 fconstmpt A × x = k A x
5 2 adantr φ x X A V
6 sneq k = A k = A
7 6 xpeq1d k = A k × x = A × x
8 opeq1 k = A k x = A x
9 8 sneqd k = A k x = A x
10 7 9 eqeq12d k = A k × x = k x A × x = A x
11 vex k V
12 vex x V
13 11 12 xpsn k × x = k x
14 10 13 vtoclg A V A × x = A x
15 5 14 syl φ x X A × x = A x
16 4 15 eqtr3id φ x X k A x = A x
17 16 mpteq2dva φ x X k A x = x X A x
18 snex A V
19 18 a1i φ A V
20 topontop J TopOn X J Top
21 3 20 syl φ J Top
22 2 21 fsnd φ A J : A Top
23 3 cnmptid φ x X x J Cn J
24 23 adantr φ k A x X x J Cn J
25 elsni k A k = A
26 25 fveq2d k A A J k = A J A
27 fvsng A V J TopOn X A J A = J
28 2 3 27 syl2anc φ A J A = J
29 26 28 sylan9eqr φ k A A J k = J
30 29 oveq2d φ k A J Cn A J k = J Cn J
31 24 30 eleqtrrd φ k A x X x J Cn A J k
32 1 3 19 22 31 ptcn φ x X k A x J Cn K
33 17 32 eqeltrrd φ x X A x J Cn K
34 simprr φ x X y = A x y = A x
35 16 adantrr φ x X y = A x k A x = A x
36 34 35 eqtr4d φ x X y = A x y = k A x
37 simprl φ x X y = A x x X
38 37 adantr φ x X y = A x k A x X
39 38 fmpttd φ x X y = A x k A x : A X
40 toponmax J TopOn X X J
41 3 40 syl φ X J
42 41 adantr φ x X y = A x X J
43 elmapg X J A V k A x X A k A x : A X
44 42 18 43 sylancl φ x X y = A x k A x X A k A x : A X
45 39 44 mpbird φ x X y = A x k A x X A
46 36 45 eqeltrd φ x X y = A x y X A
47 34 fveq1d φ x X y = A x y A = A x A
48 2 adantr φ x X y = A x A V
49 fvsng A V x X A x A = x
50 48 37 49 syl2anc φ x X y = A x A x A = x
51 47 50 eqtr2d φ x X y = A x x = y A
52 46 51 jca φ x X y = A x y X A x = y A
53 simprr φ y X A x = y A x = y A
54 simprl φ y X A x = y A y X A
55 41 adantr φ y X A x = y A X J
56 elmapg X J A V y X A y : A X
57 55 18 56 sylancl φ y X A x = y A y X A y : A X
58 54 57 mpbid φ y X A x = y A y : A X
59 snidg A V A A
60 2 59 syl φ A A
61 60 adantr φ y X A x = y A A A
62 58 61 ffvelrnd φ y X A x = y A y A X
63 53 62 eqeltrd φ y X A x = y A x X
64 2 adantr φ y X A x = y A A V
65 fsn2g A V y : A X y A X y = A y A
66 64 65 syl φ y X A x = y A y : A X y A X y = A y A
67 58 66 mpbid φ y X A x = y A y A X y = A y A
68 67 simprd φ y X A x = y A y = A y A
69 53 opeq2d φ y X A x = y A A x = A y A
70 69 sneqd φ y X A x = y A A x = A y A
71 68 70 eqtr4d φ y X A x = y A y = A x
72 63 71 jca φ y X A x = y A x X y = A x
73 52 72 impbida φ x X y = A x y X A x = y A
74 73 mptcnv φ x X A x -1 = y X A y A
75 xpsng A V J TopOn X A × J = A J
76 2 3 75 syl2anc φ A × J = A J
77 76 eqcomd φ A J = A × J
78 77 fveq2d φ 𝑡 A J = 𝑡 A × J
79 1 78 syl5eq φ K = 𝑡 A × J
80 eqid 𝑡 A × J = 𝑡 A × J
81 80 pttoponconst A V J TopOn X 𝑡 A × J TopOn X A
82 19 3 81 syl2anc φ 𝑡 A × J TopOn X A
83 79 82 eqeltrd φ K TopOn X A
84 toponuni K TopOn X A X A = K
85 83 84 syl φ X A = K
86 85 mpteq1d φ y X A y A = y K y A
87 74 86 eqtrd φ x X A x -1 = y K y A
88 eqid K = K
89 88 1 ptpjcn A V A J : A Top A A y K y A K Cn A J A
90 18 22 60 89 mp3an2i φ y K y A K Cn A J A
91 28 oveq2d φ K Cn A J A = K Cn J
92 90 91 eleqtrd φ y K y A K Cn J
93 87 92 eqeltrd φ x X A x -1 K Cn J
94 ishmeo x X A x J Homeo K x X A x J Cn K x X A x -1 K Cn J
95 33 93 94 sylanbrc φ x X A x J Homeo K