Metamath Proof Explorer


Theorem pcohtpylem

Description: Lemma for pcohtpy . (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses pcohtpy.4 φF1=G0
pcohtpy.5 φFphJH
pcohtpy.6 φGphJK
pcohtpylem.7 P=x01,y01ifx122xMy2x1Ny
pcohtpylem.8 φMFPHtpyJH
pcohtpylem.9 φNGPHtpyJK
Assertion pcohtpylem φPF*𝑝JGPHtpyJH*𝑝JK

Proof

Step Hyp Ref Expression
1 pcohtpy.4 φF1=G0
2 pcohtpy.5 φFphJH
3 pcohtpy.6 φGphJK
4 pcohtpylem.7 P=x01,y01ifx122xMy2x1Ny
5 pcohtpylem.8 φMFPHtpyJH
6 pcohtpylem.9 φNGPHtpyJK
7 isphtpc FphJHFIICnJHIICnJFPHtpyJH
8 2 7 sylib φFIICnJHIICnJFPHtpyJH
9 8 simp1d φFIICnJ
10 isphtpc GphJKGIICnJKIICnJGPHtpyJK
11 3 10 sylib φGIICnJKIICnJGPHtpyJK
12 11 simp1d φGIICnJ
13 9 12 1 pcocn φF*𝑝JGIICnJ
14 8 simp2d φHIICnJ
15 11 simp2d φKIICnJ
16 9 14 5 phtpy01 φF0=H0F1=H1
17 16 simprd φF1=H1
18 12 15 6 phtpy01 φG0=K0G1=K1
19 18 simpld φG0=K0
20 1 17 19 3eqtr3d φH1=K0
21 14 15 20 pcocn φH*𝑝JKIICnJ
22 eqid topGenran.=topGenran.
23 eqid topGenran.𝑡012=topGenran.𝑡012
24 eqid topGenran.𝑡121=topGenran.𝑡121
25 dfii2 II=topGenran.𝑡01
26 0red φ0
27 1red φ1
28 halfre 12
29 halfge0 012
30 1re 1
31 halflt1 12<1
32 28 30 31 ltleii 121
33 elicc01 120112012121
34 28 29 32 33 mpbir3an 1201
35 34 a1i φ1201
36 iitopon IITopOn01
37 36 a1i φIITopOn01
38 1 adantr φx=12y01F1=G0
39 9 14 5 phtpyi φy010My=F01My=F1
40 39 simprd φy011My=F1
41 40 adantrl φx=12y011My=F1
42 12 15 6 phtpyi φy010Ny=G01Ny=G1
43 42 simpld φy010Ny=G0
44 43 adantrl φx=12y010Ny=G0
45 38 41 44 3eqtr4d φx=12y011My=0Ny
46 simprl φx=12y01x=12
47 46 oveq2d φx=12y012x=212
48 2cn 2
49 2ne0 20
50 48 49 recidi 212=1
51 47 50 eqtrdi φx=12y012x=1
52 51 oveq1d φx=12y012xMy=1My
53 51 oveq1d φx=12y012x1=11
54 1m1e0 11=0
55 53 54 eqtrdi φx=12y012x1=0
56 55 oveq1d φx=12y012x1Ny=0Ny
57 45 52 56 3eqtr4d φx=12y012xMy=2x1Ny
58 retopon topGenran.TopOn
59 0re 0
60 iccssre 012012
61 59 28 60 mp2an 012
62 resttopon topGenran.TopOn012topGenran.𝑡012TopOn012
63 58 61 62 mp2an topGenran.𝑡012TopOn012
64 63 a1i φtopGenran.𝑡012TopOn012
65 64 37 cnmpt1st φx012,y01xtopGenran.𝑡012×tIICntopGenran.𝑡012
66 23 iihalf1cn z0122ztopGenran.𝑡012CnII
67 66 a1i φz0122ztopGenran.𝑡012CnII
68 oveq2 z=x2z=2x
69 64 37 65 64 67 68 cnmpt21 φx012,y012xtopGenran.𝑡012×tIICnII
70 64 37 cnmpt2nd φx012,y01ytopGenran.𝑡012×tIICnII
71 9 14 phtpycn φFPHtpyJHII×tIICnJ
72 71 5 sseldd φMII×tIICnJ
73 64 37 69 70 72 cnmpt22f φx012,y012xMytopGenran.𝑡012×tIICnJ
74 iccssre 121121
75 28 30 74 mp2an 121
76 resttopon topGenran.TopOn121topGenran.𝑡121TopOn121
77 58 75 76 mp2an topGenran.𝑡121TopOn121
78 77 a1i φtopGenran.𝑡121TopOn121
79 78 37 cnmpt1st φx121,y01xtopGenran.𝑡121×tIICntopGenran.𝑡121
80 24 iihalf2cn z1212z1topGenran.𝑡121CnII
81 80 a1i φz1212z1topGenran.𝑡121CnII
82 68 oveq1d z=x2z1=2x1
83 78 37 79 78 81 82 cnmpt21 φx121,y012x1topGenran.𝑡121×tIICnII
84 78 37 cnmpt2nd φx121,y01ytopGenran.𝑡121×tIICnII
85 12 15 phtpycn φGPHtpyJKII×tIICnJ
86 85 6 sseldd φNII×tIICnJ
87 78 37 83 84 86 cnmpt22f φx121,y012x1NytopGenran.𝑡121×tIICnJ
88 22 23 24 25 26 27 35 37 57 73 87 cnmpopc φx01,y01ifx122xMy2x1NyII×tIICnJ
89 4 88 eqeltrid φPII×tIICnJ
90 simpll φs01s12φ
91 elii1 s012s01s12
92 iihalf1 s0122s01
93 91 92 sylbir s01s122s01
94 93 adantll φs01s122s01
95 9 14 phtpyhtpy φFPHtpyJHFIIHtpyJH
96 95 5 sseldd φMFIIHtpyJH
97 37 9 14 96 htpyi φ2s012sM0=F2s2sM1=H2s
98 90 94 97 syl2anc φs01s122sM0=F2s2sM1=H2s
99 98 simpld φs01s122sM0=F2s
100 simpll φs01¬s12φ
101 elii2 s01¬s12s121
102 101 adantll φs01¬s12s121
103 iihalf2 s1212s101
104 102 103 syl φs01¬s122s101
105 12 15 phtpyhtpy φGPHtpyJKGIIHtpyJK
106 105 6 sseldd φNGIIHtpyJK
107 37 12 15 106 htpyi φ2s1012s1N0=G2s12s1N1=K2s1
108 100 104 107 syl2anc φs01¬s122s1N0=G2s12s1N1=K2s1
109 108 simpld φs01¬s122s1N0=G2s1
110 99 109 ifeq12da φs01ifs122sM02s1N0=ifs12F2sG2s1
111 simpr φs01s01
112 0elunit 001
113 simpl x=sy=0x=s
114 113 breq1d x=sy=0x12s12
115 113 oveq2d x=sy=02x=2s
116 simpr x=sy=0y=0
117 115 116 oveq12d x=sy=02xMy=2sM0
118 115 oveq1d x=sy=02x1=2s1
119 118 116 oveq12d x=sy=02x1Ny=2s1N0
120 114 117 119 ifbieq12d x=sy=0ifx122xMy2x1Ny=ifs122sM02s1N0
121 ovex 2sM0V
122 ovex 2s1N0V
123 121 122 ifex ifs122sM02s1N0V
124 120 4 123 ovmpoa s01001sP0=ifs122sM02s1N0
125 111 112 124 sylancl φs01sP0=ifs122sM02s1N0
126 9 12 pcovalg φs01F*𝑝JGs=ifs12F2sG2s1
127 110 125 126 3eqtr4d φs01sP0=F*𝑝JGs
128 98 simprd φs01s122sM1=H2s
129 108 simprd φs01¬s122s1N1=K2s1
130 128 129 ifeq12da φs01ifs122sM12s1N1=ifs12H2sK2s1
131 1elunit 101
132 simpl x=sy=1x=s
133 132 breq1d x=sy=1x12s12
134 132 oveq2d x=sy=12x=2s
135 simpr x=sy=1y=1
136 134 135 oveq12d x=sy=12xMy=2sM1
137 134 oveq1d x=sy=12x1=2s1
138 137 135 oveq12d x=sy=12x1Ny=2s1N1
139 133 136 138 ifbieq12d x=sy=1ifx122xMy2x1Ny=ifs122sM12s1N1
140 ovex 2sM1V
141 ovex 2s1N1V
142 140 141 ifex ifs122sM12s1N1V
143 139 4 142 ovmpoa s01101sP1=ifs122sM12s1N1
144 111 131 143 sylancl φs01sP1=ifs122sM12s1N1
145 14 15 pcovalg φs01H*𝑝JKs=ifs12H2sK2s1
146 130 144 145 3eqtr4d φs01sP1=H*𝑝JKs
147 9 14 5 phtpyi φs010Ms=F01Ms=F1
148 147 simpld φs010Ms=F0
149 simpl x=0y=sx=0
150 149 29 eqbrtrdi x=0y=sx12
151 150 iftrued x=0y=sifx122xMy2x1Ny=2xMy
152 149 oveq2d x=0y=s2x=20
153 2t0e0 20=0
154 152 153 eqtrdi x=0y=s2x=0
155 simpr x=0y=sy=s
156 154 155 oveq12d x=0y=s2xMy=0Ms
157 151 156 eqtrd x=0y=sifx122xMy2x1Ny=0Ms
158 ovex 0MsV
159 157 4 158 ovmpoa 001s010Ps=0Ms
160 112 111 159 sylancr φs010Ps=0Ms
161 9 12 pco0 φF*𝑝JG0=F0
162 161 adantr φs01F*𝑝JG0=F0
163 148 160 162 3eqtr4d φs010Ps=F*𝑝JG0
164 12 15 6 phtpyi φs010Ns=G01Ns=G1
165 164 simprd φs011Ns=G1
166 28 30 ltnlei 12<1¬112
167 31 166 mpbi ¬112
168 simpl x=1y=sx=1
169 168 breq1d x=1y=sx12112
170 167 169 mtbiri x=1y=s¬x12
171 170 iffalsed x=1y=sifx122xMy2x1Ny=2x1Ny
172 168 oveq2d x=1y=s2x=21
173 2t1e2 21=2
174 172 173 eqtrdi x=1y=s2x=2
175 174 oveq1d x=1y=s2x1=21
176 2m1e1 21=1
177 175 176 eqtrdi x=1y=s2x1=1
178 simpr x=1y=sy=s
179 177 178 oveq12d x=1y=s2x1Ny=1Ns
180 171 179 eqtrd x=1y=sifx122xMy2x1Ny=1Ns
181 ovex 1NsV
182 180 4 181 ovmpoa 101s011Ps=1Ns
183 131 111 182 sylancr φs011Ps=1Ns
184 9 12 pco1 φF*𝑝JG1=G1
185 184 adantr φs01F*𝑝JG1=G1
186 165 183 185 3eqtr4d φs011Ps=F*𝑝JG1
187 13 21 89 127 146 163 186 isphtpy2d φPF*𝑝JGPHtpyJH*𝑝JK