Metamath Proof Explorer

Theorem phtpycom

Description: Given a homotopy from F to G , produce a homotopy from G to F . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses isphtpy.2 ⊢φ→F∈IICnJ
isphtpy.3 ⊢φ→G∈IICnJ
phtpycom.6 ⊢K=x∈01,y∈01⟼xH1−y
phtpycom.7 ⊢φ→H∈FPHtpy⁡JG
Assertion phtpycom ⊢φ→K∈GPHtpy⁡JF

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢φ→F∈IICnJ
2 isphtpy.3 ⊢φ→G∈IICnJ
3 phtpycom.6 ⊢K=x∈01,y∈01⟼xH1−y
4 phtpycom.7 ⊢φ→H∈FPHtpy⁡JG
5 iitopon ⊢II∈TopOn⁡01
6 5 a1i ⊢φ→II∈TopOn⁡01
7 1 2 phtpyhtpy ⊢φ→FPHtpy⁡JG⊆FIIHtpyJG
8 7 4 sseldd ⊢φ→H∈FIIHtpyJG
9 6 1 2 3 8 htpycom ⊢φ→K∈GIIHtpyJF
10 0elunit ⊢0∈01
11 simpr ⊢φ∧t∈01→t∈01
12 oveq1 ⊢x=0→xH1−y=0H1−y
13 oveq2 ⊢y=t→1−y=1−t
14 13 oveq2d ⊢y=t→0H1−y=0H1−t
15 ovex ⊢0H1−t∈V
16 12 14 3 15 ovmpo ⊢0∈01∧t∈01→0Kt=0H1−t
17 10 11 16 sylancr ⊢φ∧t∈01→0Kt=0H1−t
18 iirev ⊢t∈01→1−t∈01
19 1 2 4 phtpyi ⊢φ∧1−t∈01→0H1−t=F⁡0∧1H1−t=F⁡1
20 18 19 sylan2 ⊢φ∧t∈01→0H1−t=F⁡0∧1H1−t=F⁡1
21 20 simpld ⊢φ∧t∈01→0H1−t=F⁡0
22 1 2 4 phtpy01 ⊢φ→F⁡0=G⁡0∧F⁡1=G⁡1
23 22 adantr ⊢φ∧t∈01→F⁡0=G⁡0∧F⁡1=G⁡1
24 23 simpld ⊢φ∧t∈01→F⁡0=G⁡0
25 17 21 24 3eqtrd ⊢φ∧t∈01→0Kt=G⁡0
26 1elunit ⊢1∈01
27 oveq1 ⊢x=1→xH1−y=1H1−y
28 13 oveq2d ⊢y=t→1H1−y=1H1−t
29 ovex ⊢1H1−t∈V
30 27 28 3 29 ovmpo ⊢1∈01∧t∈01→1Kt=1H1−t
31 26 11 30 sylancr ⊢φ∧t∈01→1Kt=1H1−t
32 20 simprd ⊢φ∧t∈01→1H1−t=F⁡1
33 23 simprd ⊢φ∧t∈01→F⁡1=G⁡1
34 31 32 33 3eqtrd ⊢φ∧t∈01→1Kt=G⁡1
35 2 1 9 25 34 isphtpyd ⊢φ→K∈GPHtpy⁡JF