# Metamath Proof Explorer

## Theorem phtpyid

Description: A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses phtpyid.1 ${⊢}{G}=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{F}\left({x}\right)\right)$
phtpyid.3 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
Assertion phtpyid ${⊢}{\phi }\to {G}\in \left({F}\mathrm{PHtpy}\left({J}\right){F}\right)$

### Proof

Step Hyp Ref Expression
1 phtpyid.1 ${⊢}{G}=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{F}\left({x}\right)\right)$
2 phtpyid.3 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
3 iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
4 3 a1i ${⊢}{\phi }\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
5 1 4 2 htpyid ${⊢}{\phi }\to {G}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){F}\right)$
6 0elunit ${⊢}0\in \left[0,1\right]$
7 fveq2 ${⊢}{x}=0\to {F}\left({x}\right)={F}\left(0\right)$
8 eqidd ${⊢}{y}={s}\to {F}\left(0\right)={F}\left(0\right)$
9 fvex ${⊢}{F}\left(0\right)\in \mathrm{V}$
10 7 8 1 9 ovmpo ${⊢}\left(0\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\to 0{G}{s}={F}\left(0\right)$
11 6 10 mpan ${⊢}{s}\in \left[0,1\right]\to 0{G}{s}={F}\left(0\right)$
12 11 adantl ${⊢}\left({\phi }\wedge {s}\in \left[0,1\right]\right)\to 0{G}{s}={F}\left(0\right)$
13 1elunit ${⊢}1\in \left[0,1\right]$
14 fveq2 ${⊢}{x}=1\to {F}\left({x}\right)={F}\left(1\right)$
15 eqidd ${⊢}{y}={s}\to {F}\left(1\right)={F}\left(1\right)$
16 fvex ${⊢}{F}\left(1\right)\in \mathrm{V}$
17 14 15 1 16 ovmpo ${⊢}\left(1\in \left[0,1\right]\wedge {s}\in \left[0,1\right]\right)\to 1{G}{s}={F}\left(1\right)$
18 13 17 mpan ${⊢}{s}\in \left[0,1\right]\to 1{G}{s}={F}\left(1\right)$
19 18 adantl ${⊢}\left({\phi }\wedge {s}\in \left[0,1\right]\right)\to 1{G}{s}={F}\left(1\right)$
20 2 2 5 12 19 isphtpyd ${⊢}{\phi }\to {G}\in \left({F}\mathrm{PHtpy}\left({J}\right){F}\right)$