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 = 0 1 × Y
Assertion pcopt F II Cn J F 0 = Y P * 𝑝 J F ph J F

Proof

Step Hyp Ref Expression
1 pcopt.1 P = 0 1 × Y
2 1 fveq1i P 2 x = 0 1 × Y 2 x
3 simpr F II Cn J F 0 = Y F 0 = Y
4 iiuni 0 1 = II
5 eqid J = J
6 4 5 cnf F II Cn J F : 0 1 J
7 6 adantr F II Cn J F 0 = Y F : 0 1 J
8 0elunit 0 0 1
9 ffvelrn F : 0 1 J 0 0 1 F 0 J
10 7 8 9 sylancl F II Cn J F 0 = Y F 0 J
11 3 10 eqeltrrd F II Cn J F 0 = Y Y J
12 elii1 x 0 1 2 x 0 1 x 1 2
13 iihalf1 x 0 1 2 2 x 0 1
14 12 13 sylbir x 0 1 x 1 2 2 x 0 1
15 fvconst2g Y J 2 x 0 1 0 1 × Y 2 x = Y
16 11 14 15 syl2an F II Cn J F 0 = Y x 0 1 x 1 2 0 1 × Y 2 x = Y
17 2 16 syl5eq F II Cn J F 0 = Y x 0 1 x 1 2 P 2 x = Y
18 simplr F II Cn J F 0 = Y x 0 1 x 1 2 F 0 = Y
19 17 18 eqtr4d F II Cn J F 0 = Y x 0 1 x 1 2 P 2 x = F 0
20 19 ifeq1d F II Cn J F 0 = Y x 0 1 x 1 2 if x 1 2 P 2 x F 2 x 1 = if x 1 2 F 0 F 2 x 1
21 20 expr F II Cn J F 0 = Y x 0 1 x 1 2 if x 1 2 P 2 x F 2 x 1 = if x 1 2 F 0 F 2 x 1
22 iffalse ¬ x 1 2 if x 1 2 P 2 x F 2 x 1 = F 2 x 1
23 iffalse ¬ x 1 2 if x 1 2 F 0 F 2 x 1 = F 2 x 1
24 22 23 eqtr4d ¬ x 1 2 if x 1 2 P 2 x F 2 x 1 = if x 1 2 F 0 F 2 x 1
25 21 24 pm2.61d1 F II Cn J F 0 = Y x 0 1 if x 1 2 P 2 x F 2 x 1 = if x 1 2 F 0 F 2 x 1
26 25 mpteq2dva F II Cn J F 0 = Y x 0 1 if x 1 2 P 2 x F 2 x 1 = x 0 1 if x 1 2 F 0 F 2 x 1
27 cntop2 F II Cn J J Top
28 27 adantr F II Cn J F 0 = Y J Top
29 toptopon2 J Top J TopOn J
30 28 29 sylib F II Cn J F 0 = Y J TopOn J
31 1 pcoptcl J TopOn J Y J P II Cn J P 0 = Y P 1 = Y
32 30 11 31 syl2anc F II Cn J F 0 = Y P II Cn J P 0 = Y P 1 = Y
33 32 simp1d F II Cn J F 0 = Y P II Cn J
34 simpl F II Cn J F 0 = Y F II Cn J
35 33 34 pcoval F II Cn J F 0 = Y P * 𝑝 J F = x 0 1 if x 1 2 P 2 x F 2 x 1
36 iffalse ¬ x 1 2 if x 1 2 0 2 x 1 = 2 x 1
37 36 adantl x 0 1 ¬ x 1 2 if x 1 2 0 2 x 1 = 2 x 1
38 elii2 x 0 1 ¬ x 1 2 x 1 2 1
39 iihalf2 x 1 2 1 2 x 1 0 1
40 38 39 syl x 0 1 ¬ x 1 2 2 x 1 0 1
41 37 40 eqeltrd x 0 1 ¬ x 1 2 if x 1 2 0 2 x 1 0 1
42 41 ex x 0 1 ¬ x 1 2 if x 1 2 0 2 x 1 0 1
43 iftrue x 1 2 if x 1 2 0 2 x 1 = 0
44 43 8 eqeltrdi x 1 2 if x 1 2 0 2 x 1 0 1
45 42 44 pm2.61d2 x 0 1 if x 1 2 0 2 x 1 0 1
46 45 adantl F II Cn J F 0 = Y x 0 1 if x 1 2 0 2 x 1 0 1
47 eqid x 0 1 if x 1 2 0 2 x 1 = x 0 1 if x 1 2 0 2 x 1
48 47 a1i F II Cn J F 0 = Y x 0 1 if x 1 2 0 2 x 1 = x 0 1 if x 1 2 0 2 x 1
49 7 feqmptd F II Cn J F 0 = Y F = y 0 1 F y
50 fveq2 y = if x 1 2 0 2 x 1 F y = F if x 1 2 0 2 x 1
51 fvif F if x 1 2 0 2 x 1 = if x 1 2 F 0 F 2 x 1
52 50 51 eqtrdi y = if x 1 2 0 2 x 1 F y = if x 1 2 F 0 F 2 x 1
53 46 48 49 52 fmptco F II Cn J F 0 = Y F x 0 1 if x 1 2 0 2 x 1 = x 0 1 if x 1 2 F 0 F 2 x 1
54 26 35 53 3eqtr4d F II Cn J F 0 = Y P * 𝑝 J F = F x 0 1 if x 1 2 0 2 x 1
55 iitopon II TopOn 0 1
56 55 a1i F II Cn J F 0 = Y II TopOn 0 1
57 56 cnmptid F II Cn J F 0 = Y x 0 1 x II Cn II
58 8 a1i F II Cn J F 0 = Y 0 0 1
59 56 56 58 cnmptc F II Cn J F 0 = Y x 0 1 0 II Cn II
60 eqid topGen ran . = topGen ran .
61 eqid topGen ran . 𝑡 0 1 2 = topGen ran . 𝑡 0 1 2
62 eqid topGen ran . 𝑡 1 2 1 = topGen ran . 𝑡 1 2 1
63 dfii2 II = topGen ran . 𝑡 0 1
64 0re 0
65 64 a1i F II Cn J F 0 = Y 0
66 1re 1
67 66 a1i F II Cn J F 0 = Y 1
68 halfre 1 2
69 halfge0 0 1 2
70 halflt1 1 2 < 1
71 68 66 70 ltleii 1 2 1
72 elicc01 1 2 0 1 1 2 0 1 2 1 2 1
73 68 69 71 72 mpbir3an 1 2 0 1
74 73 a1i F II Cn J F 0 = Y 1 2 0 1
75 simprl F II Cn J F 0 = Y y = 1 2 z 0 1 y = 1 2
76 75 oveq2d F II Cn J F 0 = Y y = 1 2 z 0 1 2 y = 2 1 2
77 2cn 2
78 2ne0 2 0
79 77 78 recidi 2 1 2 = 1
80 76 79 eqtrdi F II Cn J F 0 = Y y = 1 2 z 0 1 2 y = 1
81 80 oveq1d F II Cn J F 0 = Y y = 1 2 z 0 1 2 y 1 = 1 1
82 1m1e0 1 1 = 0
83 81 82 eqtr2di F II Cn J F 0 = Y y = 1 2 z 0 1 0 = 2 y 1
84 retopon topGen ran . TopOn
85 iccssre 0 1 2 0 1 2
86 64 68 85 mp2an 0 1 2
87 resttopon topGen ran . TopOn 0 1 2 topGen ran . 𝑡 0 1 2 TopOn 0 1 2
88 84 86 87 mp2an topGen ran . 𝑡 0 1 2 TopOn 0 1 2
89 88 a1i F II Cn J F 0 = Y topGen ran . 𝑡 0 1 2 TopOn 0 1 2
90 89 56 56 58 cnmpt2c F II Cn J F 0 = Y y 0 1 2 , z 0 1 0 topGen ran . 𝑡 0 1 2 × t II Cn II
91 iccssre 1 2 1 1 2 1
92 68 66 91 mp2an 1 2 1
93 resttopon topGen ran . TopOn 1 2 1 topGen ran . 𝑡 1 2 1 TopOn 1 2 1
94 84 92 93 mp2an topGen ran . 𝑡 1 2 1 TopOn 1 2 1
95 94 a1i F II Cn J F 0 = Y topGen ran . 𝑡 1 2 1 TopOn 1 2 1
96 95 56 cnmpt1st F II Cn J F 0 = Y y 1 2 1 , z 0 1 y topGen ran . 𝑡 1 2 1 × t II Cn topGen ran . 𝑡 1 2 1
97 62 iihalf2cn x 1 2 1 2 x 1 topGen ran . 𝑡 1 2 1 Cn II
98 97 a1i F II Cn J F 0 = Y x 1 2 1 2 x 1 topGen ran . 𝑡 1 2 1 Cn II
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 II Cn J F 0 = Y y 1 2 1 , z 0 1 2 y 1 topGen ran . 𝑡 1 2 1 × t II Cn II
102 60 61 62 63 65 67 74 56 83 90 101 cnmpopc F II Cn J F 0 = Y y 0 1 , z 0 1 if y 1 2 0 2 y 1 II × t II Cn II
103 breq1 y = x y 1 2 x 1 2
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 if y 1 2 0 2 y 1 = if x 1 2 0 2 x 1
107 106 adantr y = x z = 0 if y 1 2 0 2 y 1 = if x 1 2 0 2 x 1
108 56 57 59 56 56 102 107 cnmpt12 F II Cn J F 0 = Y x 0 1 if x 1 2 0 2 x 1 II Cn II
109 id x = 0 x = 0
110 109 69 eqbrtrdi x = 0 x 1 2
111 110 43 syl x = 0 if x 1 2 0 2 x 1 = 0
112 c0ex 0 V
113 111 47 112 fvmpt 0 0 1 x 0 1 if x 1 2 0 2 x 1 0 = 0
114 8 113 mp1i F II Cn J F 0 = Y x 0 1 if x 1 2 0 2 x 1 0 = 0
115 1elunit 1 0 1
116 68 66 ltnlei 1 2 < 1 ¬ 1 1 2
117 70 116 mpbi ¬ 1 1 2
118 breq1 x = 1 x 1 2 1 1 2
119 117 118 mtbiri x = 1 ¬ x 1 2
120 119 36 syl x = 1 if x 1 2 0 2 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 if x 1 2 0 2 x 1 = 1
128 1ex 1 V
129 127 47 128 fvmpt 1 0 1 x 0 1 if x 1 2 0 2 x 1 1 = 1
130 115 129 mp1i F II Cn J F 0 = Y x 0 1 if x 1 2 0 2 x 1 1 = 1
131 34 108 114 130 reparpht F II Cn J F 0 = Y F x 0 1 if x 1 2 0 2 x 1 ph J F
132 54 131 eqbrtrd F II Cn J F 0 = Y P * 𝑝 J F ph J F