Metamath Proof Explorer

Theorem pcopt

Description: Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 20-Dec-2013)

Ref Expression
Hypothesis pcopt.1 ⊢P=01×Y
Assertion pcopt ⊢F∈IICnJ∧F⁡0=Y→P*𝑝⁡JF≃ph⁡JF

Proof

Step Hyp Ref Expression
1 pcopt.1 ⊢P=01×Y
2 1 fveq1i ⊢P⁡2⁢x=01×Y⁡2⁢x
3 simpr ⊢F∈IICnJ∧F⁡0=Y→F⁡0=Y
4 iiuni ⊢01=⋃II
5 eqid ⊢⋃J=⋃J
6 4 5 cnf ⊢F∈IICnJ→F:01⟶⋃J
7 6 adantr ⊢F∈IICnJ∧F⁡0=Y→F:01⟶⋃J
8 0elunit ⊢0∈01
9 ffvelcdm ⊢F:01⟶⋃J∧0∈01→F⁡0∈⋃J
10 7 8 9 sylancl ⊢F∈IICnJ∧F⁡0=Y→F⁡0∈⋃J
11 3 10 eqeltrrd ⊢F∈IICnJ∧F⁡0=Y→Y∈⋃J
12 elii1 ⊢x∈012↔x∈01∧x≤12
13 iihalf1 ⊢x∈012→2⁢x∈01
14 12 13 sylbir ⊢x∈01∧x≤12→2⁢x∈01
15 fvconst2g ⊢Y∈⋃J∧2⁢x∈01→01×Y⁡2⁢x=Y
16 11 14 15 syl2an ⊢F∈IICnJ∧F⁡0=Y∧x∈01∧x≤12→01×Y⁡2⁢x=Y
17 2 16 eqtrid ⊢F∈IICnJ∧F⁡0=Y∧x∈01∧x≤12→P⁡2⁢x=Y
18 simplr ⊢F∈IICnJ∧F⁡0=Y∧x∈01∧x≤12→F⁡0=Y
19 17 18 eqtr4d ⊢F∈IICnJ∧F⁡0=Y∧x∈01∧x≤12→P⁡2⁢x=F⁡0
20 19 ifeq1d ⊢F∈IICnJ∧F⁡0=Y∧x∈01∧x≤12→ifx≤12P⁡2⁢xF⁡2⁢x−1=ifx≤12F⁡0F⁡2⁢x−1
21 20 expr ⊢F∈IICnJ∧F⁡0=Y∧x∈01→x≤12→ifx≤12P⁡2⁢xF⁡2⁢x−1=ifx≤12F⁡0F⁡2⁢x−1
22 iffalse ⊢¬x≤12→ifx≤12P⁡2⁢xF⁡2⁢x−1=F⁡2⁢x−1
23 iffalse ⊢¬x≤12→ifx≤12F⁡0F⁡2⁢x−1=F⁡2⁢x−1
24 22 23 eqtr4d ⊢¬x≤12→ifx≤12P⁡2⁢xF⁡2⁢x−1=ifx≤12F⁡0F⁡2⁢x−1
25 21 24 pm2.61d1 ⊢F∈IICnJ∧F⁡0=Y∧x∈01→ifx≤12P⁡2⁢xF⁡2⁢x−1=ifx≤12F⁡0F⁡2⁢x−1
26 25 mpteq2dva ⊢F∈IICnJ∧F⁡0=Y→x∈01⟼ifx≤12P⁡2⁢xF⁡2⁢x−1=x∈01⟼ifx≤12F⁡0F⁡2⁢x−1
27 cntop2 ⊢F∈IICnJ→J∈Top
28 27 adantr ⊢F∈IICnJ∧F⁡0=Y→J∈Top
29 toptopon2 ⊢J∈Top↔J∈TopOn⁡⋃J
30 28 29 sylib ⊢F∈IICnJ∧F⁡0=Y→J∈TopOn⁡⋃J
31 1 pcoptcl ⊢J∈TopOn⁡⋃J∧Y∈⋃J→P∈IICnJ∧P⁡0=Y∧P⁡1=Y
32 30 11 31 syl2anc ⊢F∈IICnJ∧F⁡0=Y→P∈IICnJ∧P⁡0=Y∧P⁡1=Y
33 32 simp1d ⊢F∈IICnJ∧F⁡0=Y→P∈IICnJ
34 simpl ⊢F∈IICnJ∧F⁡0=Y→F∈IICnJ
35 33 34 pcoval ⊢F∈IICnJ∧F⁡0=Y→P*𝑝⁡JF=x∈01⟼ifx≤12P⁡2⁢xF⁡2⁢x−1
36 iffalse ⊢¬x≤12→ifx≤1202⁢x−1=2⁢x−1
37 36 adantl ⊢x∈01∧¬x≤12→ifx≤1202⁢x−1=2⁢x−1
38 elii2 ⊢x∈01∧¬x≤12→x∈121
39 iihalf2 ⊢x∈121→2⁢x−1∈01
40 38 39 syl ⊢x∈01∧¬x≤12→2⁢x−1∈01
41 37 40 eqeltrd ⊢x∈01∧¬x≤12→ifx≤1202⁢x−1∈01
42 41 ex ⊢x∈01→¬x≤12→ifx≤1202⁢x−1∈01
43 iftrue ⊢x≤12→ifx≤1202⁢x−1=0
44 43 8 eqeltrdi ⊢x≤12→ifx≤1202⁢x−1∈01
45 42 44 pm2.61d2 ⊢x∈01→ifx≤1202⁢x−1∈01
46 45 adantl ⊢F∈IICnJ∧F⁡0=Y∧x∈01→ifx≤1202⁢x−1∈01
47 eqid ⊢x∈01⟼ifx≤1202⁢x−1=x∈01⟼ifx≤1202⁢x−1
48 47 a1i ⊢F∈IICnJ∧F⁡0=Y→x∈01⟼ifx≤1202⁢x−1=x∈01⟼ifx≤1202⁢x−1
49 7 feqmptd ⊢F∈IICnJ∧F⁡0=Y→F=y∈01⟼F⁡y
50 fveq2 ⊢y=ifx≤1202⁢x−1→F⁡y=F⁡ifx≤1202⁢x−1
51 fvif ⊢F⁡ifx≤1202⁢x−1=ifx≤12F⁡0F⁡2⁢x−1
52 50 51 eqtrdi ⊢y=ifx≤1202⁢x−1→F⁡y=ifx≤12F⁡0F⁡2⁢x−1
53 46 48 49 52 fmptco ⊢F∈IICnJ∧F⁡0=Y→F∘x∈01⟼ifx≤1202⁢x−1=x∈01⟼ifx≤12F⁡0F⁡2⁢x−1
54 26 35 53 3eqtr4d ⊢F∈IICnJ∧F⁡0=Y→P*𝑝⁡JF=F∘x∈01⟼ifx≤1202⁢x−1
55 iitopon ⊢II∈TopOn⁡01
56 55 a1i ⊢F∈IICnJ∧F⁡0=Y→II∈TopOn⁡01
57 56 cnmptid ⊢F∈IICnJ∧F⁡0=Y→x∈01⟼x∈IICnII
58 8 a1i ⊢F∈IICnJ∧F⁡0=Y→0∈01
59 56 56 58 cnmptc ⊢F∈IICnJ∧F⁡0=Y→x∈01⟼0∈IICnII
60 eqid ⊢topGen⁡ran⁡.=topGen⁡ran⁡.
61 eqid ⊢topGen⁡ran⁡.↾𝑡012=topGen⁡ran⁡.↾𝑡012
62 eqid ⊢topGen⁡ran⁡.↾𝑡121=topGen⁡ran⁡.↾𝑡121
63 dfii2 ⊢II=topGen⁡ran⁡.↾𝑡01
64 0re ⊢0∈ℝ
65 64 a1i ⊢F∈IICnJ∧F⁡0=Y→0∈ℝ
66 1re ⊢1∈ℝ
67 66 a1i ⊢F∈IICnJ∧F⁡0=Y→1∈ℝ
68 halfre ⊢12∈ℝ
69 halfge0 ⊢0≤12
70 halflt1 ⊢12<1
71 68 66 70 ltleii ⊢12≤1
72 elicc01 ⊢12∈01↔12∈ℝ∧0≤12∧12≤1
73 68 69 71 72 mpbir3an ⊢12∈01
74 73 a1i ⊢F∈IICnJ∧F⁡0=Y→12∈01
75 simprl ⊢F∈IICnJ∧F⁡0=Y∧y=12∧z∈01→y=12
76 75 oveq2d ⊢F∈IICnJ∧F⁡0=Y∧y=12∧z∈01→2⁢y=2⁢12
77 2cn ⊢2∈ℂ
78 2ne0 ⊢2≠0
79 77 78 recidi ⊢2⁢12=1
80 76 79 eqtrdi ⊢F∈IICnJ∧F⁡0=Y∧y=12∧z∈01→2⁢y=1
81 80 oveq1d ⊢F∈IICnJ∧F⁡0=Y∧y=12∧z∈01→2⁢y−1=1−1
82 1m1e0 ⊢1−1=0
83 81 82 eqtr2di ⊢F∈IICnJ∧F⁡0=Y∧y=12∧z∈01→0=2⁢y−1
84 retopon ⊢topGen⁡ran⁡.∈TopOn⁡ℝ
85 iccssre ⊢0∈ℝ∧12∈ℝ→012⊆ℝ
86 64 68 85 mp2an ⊢012⊆ℝ
87 resttopon ⊢topGen⁡ran⁡.∈TopOn⁡ℝ∧012⊆ℝ→topGen⁡ran⁡.↾𝑡012∈TopOn⁡012
88 84 86 87 mp2an ⊢topGen⁡ran⁡.↾𝑡012∈TopOn⁡012
89 88 a1i ⊢F∈IICnJ∧F⁡0=Y→topGen⁡ran⁡.↾𝑡012∈TopOn⁡012
90 89 56 56 58 cnmpt2c ⊢F∈IICnJ∧F⁡0=Y→y∈012,z∈01⟼0∈topGen⁡ran⁡.↾𝑡012×tIICnII
91 iccssre ⊢12∈ℝ∧1∈ℝ→121⊆ℝ
92 68 66 91 mp2an ⊢121⊆ℝ
93 resttopon ⊢topGen⁡ran⁡.∈TopOn⁡ℝ∧121⊆ℝ→topGen⁡ran⁡.↾𝑡121∈TopOn⁡121
94 84 92 93 mp2an ⊢topGen⁡ran⁡.↾𝑡121∈TopOn⁡121
95 94 a1i ⊢F∈IICnJ∧F⁡0=Y→topGen⁡ran⁡.↾𝑡121∈TopOn⁡121
96 95 56 cnmpt1st ⊢F∈IICnJ∧F⁡0=Y→y∈121,z∈01⟼y∈topGen⁡ran⁡.↾𝑡121×tIICntopGen⁡ran⁡.↾𝑡121
97 62 iihalf2cn ⊢x∈121⟼2⁢x−1∈topGen⁡ran⁡.↾𝑡121CnII
98 97 a1i ⊢F∈IICnJ∧F⁡0=Y→x∈121⟼2⁢x−1∈topGen⁡ran⁡.↾𝑡121CnII
99 oveq2 ⊢x=y→2⁢x=2⁢y
100 99 oveq1d ⊢x=y→2⁢x−1=2⁢y−1
101 95 56 96 95 98 100 cnmpt21 ⊢F∈IICnJ∧F⁡0=Y→y∈121,z∈01⟼2⁢y−1∈topGen⁡ran⁡.↾𝑡121×tIICnII
102 60 61 62 63 65 67 74 56 83 90 101 cnmpopc ⊢F∈IICnJ∧F⁡0=Y→y∈01,z∈01⟼ify≤1202⁢y−1∈II×tIICnII
103 breq1 ⊢y=x→y≤12↔x≤12
104 oveq2 ⊢y=x→2⁢y=2⁢x
105 104 oveq1d ⊢y=x→2⁢y−1=2⁢x−1
106 103 105 ifbieq2d ⊢y=x→ify≤1202⁢y−1=ifx≤1202⁢x−1
107 106 adantr ⊢y=x∧z=0→ify≤1202⁢y−1=ifx≤1202⁢x−1
108 56 57 59 56 56 102 107 cnmpt12 ⊢F∈IICnJ∧F⁡0=Y→x∈01⟼ifx≤1202⁢x−1∈IICnII
109 id ⊢x=0→x=0
110 109 69 eqbrtrdi ⊢x=0→x≤12
111 110 43 syl ⊢x=0→ifx≤1202⁢x−1=0
112 c0ex ⊢0∈V
113 111 47 112 fvmpt ⊢0∈01→x∈01⟼ifx≤1202⁢x−1⁡0=0
114 8 113 mp1i ⊢F∈IICnJ∧F⁡0=Y→x∈01⟼ifx≤1202⁢x−1⁡0=0
115 1elunit ⊢1∈01
116 68 66 ltnlei ⊢12<1↔¬1≤12
117 70 116 mpbi ⊢¬1≤12
118 breq1 ⊢x=1→x≤12↔1≤12
119 117 118 mtbiri ⊢x=1→¬x≤12
120 119 36 syl ⊢x=1→ifx≤1202⁢x−1=2⁢x−1
121 oveq2 ⊢x=1→2⁢x=2⋅1
122 2t1e2 ⊢2⋅1=2
123 121 122 eqtrdi ⊢x=1→2⁢x=2
124 123 oveq1d ⊢x=1→2⁢x−1=2−1
125 2m1e1 ⊢2−1=1
126 124 125 eqtrdi ⊢x=1→2⁢x−1=1
127 120 126 eqtrd ⊢x=1→ifx≤1202⁢x−1=1
128 1ex ⊢1∈V
129 127 47 128 fvmpt ⊢1∈01→x∈01⟼ifx≤1202⁢x−1⁡1=1
130 115 129 mp1i ⊢F∈IICnJ∧F⁡0=Y→x∈01⟼ifx≤1202⁢x−1⁡1=1
131 34 108 114 130 reparpht ⊢F∈IICnJ∧F⁡0=Y→F∘x∈01⟼ifx≤1202⁢x−1≃ph⁡JF
132 54 131 eqbrtrd ⊢F∈IICnJ∧F⁡0=Y→P*𝑝⁡JF≃ph⁡JF