# Metamath Proof Explorer

## Theorem htpycom

Description: Given a homotopy from F to G , produce a homotopy from G to F . (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses ishtpy.1 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
ishtpy.3 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
ishtpy.4 ${⊢}{\phi }\to {G}\in \left({J}\mathrm{Cn}{K}\right)$
htpycom.6 ${⊢}{M}=\left({x}\in {X},{y}\in \left[0,1\right]⟼{x}{H}\left(1-{y}\right)\right)$
htpycom.7 ${⊢}{\phi }\to {H}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){G}\right)$
Assertion htpycom ${⊢}{\phi }\to {M}\in \left({G}\left({J}\mathrm{Htpy}{K}\right){F}\right)$

### Proof

Step Hyp Ref Expression
1 ishtpy.1 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
2 ishtpy.3 ${⊢}{\phi }\to {F}\in \left({J}\mathrm{Cn}{K}\right)$
3 ishtpy.4 ${⊢}{\phi }\to {G}\in \left({J}\mathrm{Cn}{K}\right)$
4 htpycom.6 ${⊢}{M}=\left({x}\in {X},{y}\in \left[0,1\right]⟼{x}{H}\left(1-{y}\right)\right)$
5 htpycom.7 ${⊢}{\phi }\to {H}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){G}\right)$
6 iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
7 6 a1i ${⊢}{\phi }\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
8 1 7 cnmpt1st ${⊢}{\phi }\to \left({x}\in {X},{y}\in \left[0,1\right]⟼{x}\right)\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
9 1 7 cnmpt2nd ${⊢}{\phi }\to \left({x}\in {X},{y}\in \left[0,1\right]⟼{y}\right)\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{II}\right)$
10 iirevcn ${⊢}\left({z}\in \left[0,1\right]⟼1-{z}\right)\in \left(\mathrm{II}\mathrm{Cn}\mathrm{II}\right)$
11 10 a1i ${⊢}{\phi }\to \left({z}\in \left[0,1\right]⟼1-{z}\right)\in \left(\mathrm{II}\mathrm{Cn}\mathrm{II}\right)$
12 oveq2 ${⊢}{z}={y}\to 1-{z}=1-{y}$
13 1 7 9 7 11 12 cnmpt21 ${⊢}{\phi }\to \left({x}\in {X},{y}\in \left[0,1\right]⟼1-{y}\right)\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{II}\right)$
14 1 2 3 htpycn ${⊢}{\phi }\to {F}\left({J}\mathrm{Htpy}{K}\right){G}\subseteq \left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}$
15 14 5 sseldd ${⊢}{\phi }\to {H}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)$
16 1 7 8 13 15 cnmpt22f ${⊢}{\phi }\to \left({x}\in {X},{y}\in \left[0,1\right]⟼{x}{H}\left(1-{y}\right)\right)\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)$
17 4 16 eqeltrid ${⊢}{\phi }\to {M}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)$
18 simpr ${⊢}\left({\phi }\wedge {t}\in {X}\right)\to {t}\in {X}$
19 0elunit ${⊢}0\in \left[0,1\right]$
20 oveq1 ${⊢}{x}={t}\to {x}{H}\left(1-{y}\right)={t}{H}\left(1-{y}\right)$
21 oveq2 ${⊢}{y}=0\to 1-{y}=1-0$
22 1m0e1 ${⊢}1-0=1$
23 21 22 syl6eq ${⊢}{y}=0\to 1-{y}=1$
24 23 oveq2d ${⊢}{y}=0\to {t}{H}\left(1-{y}\right)={t}{H}1$
25 ovex ${⊢}{t}{H}1\in \mathrm{V}$
26 20 24 4 25 ovmpo ${⊢}\left({t}\in {X}\wedge 0\in \left[0,1\right]\right)\to {t}{M}0={t}{H}1$
27 18 19 26 sylancl ${⊢}\left({\phi }\wedge {t}\in {X}\right)\to {t}{M}0={t}{H}1$
28 1 2 3 5 htpyi ${⊢}\left({\phi }\wedge {t}\in {X}\right)\to \left({t}{H}0={F}\left({t}\right)\wedge {t}{H}1={G}\left({t}\right)\right)$
29 28 simprd ${⊢}\left({\phi }\wedge {t}\in {X}\right)\to {t}{H}1={G}\left({t}\right)$
30 27 29 eqtrd ${⊢}\left({\phi }\wedge {t}\in {X}\right)\to {t}{M}0={G}\left({t}\right)$
31 1elunit ${⊢}1\in \left[0,1\right]$
32 oveq2 ${⊢}{y}=1\to 1-{y}=1-1$
33 1m1e0 ${⊢}1-1=0$
34 32 33 syl6eq ${⊢}{y}=1\to 1-{y}=0$
35 34 oveq2d ${⊢}{y}=1\to {t}{H}\left(1-{y}\right)={t}{H}0$
36 ovex ${⊢}{t}{H}0\in \mathrm{V}$
37 20 35 4 36 ovmpo ${⊢}\left({t}\in {X}\wedge 1\in \left[0,1\right]\right)\to {t}{M}1={t}{H}0$
38 18 31 37 sylancl ${⊢}\left({\phi }\wedge {t}\in {X}\right)\to {t}{M}1={t}{H}0$
39 28 simpld ${⊢}\left({\phi }\wedge {t}\in {X}\right)\to {t}{H}0={F}\left({t}\right)$
40 38 39 eqtrd ${⊢}\left({\phi }\wedge {t}\in {X}\right)\to {t}{M}1={F}\left({t}\right)$
41 1 3 2 17 30 40 ishtpyd ${⊢}{\phi }\to {M}\in \left({G}\left({J}\mathrm{Htpy}{K}\right){F}\right)$