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 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
isphtpy.3 ${⊢}{\phi }\to {G}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
phtpycom.6 ${⊢}{K}=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{H}\left(1-{y}\right)\right)$
phtpycom.7 ${⊢}{\phi }\to {H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)$
Assertion phtpycom ${⊢}{\phi }\to {K}\in \left({G}\mathrm{PHtpy}\left({J}\right){F}\right)$

Proof

Step Hyp Ref Expression
1 isphtpy.2 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
2 isphtpy.3 ${⊢}{\phi }\to {G}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
3 phtpycom.6 ${⊢}{K}=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{H}\left(1-{y}\right)\right)$
4 phtpycom.7 ${⊢}{\phi }\to {H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)$
5 iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
6 5 a1i ${⊢}{\phi }\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
7 1 2 phtpyhtpy ${⊢}{\phi }\to {F}\mathrm{PHtpy}\left({J}\right){G}\subseteq {F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}$
8 7 4 sseldd ${⊢}{\phi }\to {H}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)$
9 6 1 2 3 8 htpycom ${⊢}{\phi }\to {K}\in \left({G}\left(\mathrm{II}\mathrm{Htpy}{J}\right){F}\right)$
10 0elunit ${⊢}0\in \left[0,1\right]$
11 simpr ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to {t}\in \left[0,1\right]$
12 oveq1 ${⊢}{x}=0\to {x}{H}\left(1-{y}\right)=0{H}\left(1-{y}\right)$
13 oveq2 ${⊢}{y}={t}\to 1-{y}=1-{t}$
14 13 oveq2d ${⊢}{y}={t}\to 0{H}\left(1-{y}\right)=0{H}\left(1-{t}\right)$
15 ovex ${⊢}0{H}\left(1-{t}\right)\in \mathrm{V}$
16 12 14 3 15 ovmpo ${⊢}\left(0\in \left[0,1\right]\wedge {t}\in \left[0,1\right]\right)\to 0{K}{t}=0{H}\left(1-{t}\right)$
17 10 11 16 sylancr ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to 0{K}{t}=0{H}\left(1-{t}\right)$
18 iirev ${⊢}{t}\in \left[0,1\right]\to 1-{t}\in \left[0,1\right]$
19 1 2 4 phtpyi ${⊢}\left({\phi }\wedge 1-{t}\in \left[0,1\right]\right)\to \left(0{H}\left(1-{t}\right)={F}\left(0\right)\wedge 1{H}\left(1-{t}\right)={F}\left(1\right)\right)$
20 18 19 sylan2 ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to \left(0{H}\left(1-{t}\right)={F}\left(0\right)\wedge 1{H}\left(1-{t}\right)={F}\left(1\right)\right)$
21 20 simpld ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to 0{H}\left(1-{t}\right)={F}\left(0\right)$
22 1 2 4 phtpy01 ${⊢}{\phi }\to \left({F}\left(0\right)={G}\left(0\right)\wedge {F}\left(1\right)={G}\left(1\right)\right)$
23 22 adantr ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to \left({F}\left(0\right)={G}\left(0\right)\wedge {F}\left(1\right)={G}\left(1\right)\right)$
24 23 simpld ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to {F}\left(0\right)={G}\left(0\right)$
25 17 21 24 3eqtrd ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to 0{K}{t}={G}\left(0\right)$
26 1elunit ${⊢}1\in \left[0,1\right]$
27 oveq1 ${⊢}{x}=1\to {x}{H}\left(1-{y}\right)=1{H}\left(1-{y}\right)$
28 13 oveq2d ${⊢}{y}={t}\to 1{H}\left(1-{y}\right)=1{H}\left(1-{t}\right)$
29 ovex ${⊢}1{H}\left(1-{t}\right)\in \mathrm{V}$
30 27 28 3 29 ovmpo ${⊢}\left(1\in \left[0,1\right]\wedge {t}\in \left[0,1\right]\right)\to 1{K}{t}=1{H}\left(1-{t}\right)$
31 26 11 30 sylancr ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to 1{K}{t}=1{H}\left(1-{t}\right)$
32 20 simprd ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to 1{H}\left(1-{t}\right)={F}\left(1\right)$
33 23 simprd ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to {F}\left(1\right)={G}\left(1\right)$
34 31 32 33 3eqtrd ${⊢}\left({\phi }\wedge {t}\in \left[0,1\right]\right)\to 1{K}{t}={G}\left(1\right)$
35 2 1 9 25 34 isphtpyd ${⊢}{\phi }\to {K}\in \left({G}\mathrm{PHtpy}\left({J}\right){F}\right)$