# Metamath Proof Explorer

## Theorem phtpyi

Description: Membership in the class of path homotopies between two continuous functions. (Contributed 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)$
phtpyi.1 ${⊢}{\phi }\to {H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)$
Assertion phtpyi ${⊢}\left({\phi }\wedge {A}\in \left[0,1\right]\right)\to \left(0{H}{A}={F}\left(0\right)\wedge 1{H}{A}={F}\left(1\right)\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 phtpyi.1 ${⊢}{\phi }\to {H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)$
4 1 2 isphtpy ${⊢}{\phi }\to \left({H}\in \left({F}\mathrm{PHtpy}\left({J}\right){G}\right)↔\left({H}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)\wedge \forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)\right)\right)$
5 3 4 mpbid ${⊢}{\phi }\to \left({H}\in \left({F}\left(\mathrm{II}\mathrm{Htpy}{J}\right){G}\right)\wedge \forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)\right)$
6 5 simprd ${⊢}{\phi }\to \forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)$
7 oveq2 ${⊢}{s}={A}\to 0{H}{s}=0{H}{A}$
8 7 eqeq1d ${⊢}{s}={A}\to \left(0{H}{s}={F}\left(0\right)↔0{H}{A}={F}\left(0\right)\right)$
9 oveq2 ${⊢}{s}={A}\to 1{H}{s}=1{H}{A}$
10 9 eqeq1d ${⊢}{s}={A}\to \left(1{H}{s}={F}\left(1\right)↔1{H}{A}={F}\left(1\right)\right)$
11 8 10 anbi12d ${⊢}{s}={A}\to \left(\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)↔\left(0{H}{A}={F}\left(0\right)\wedge 1{H}{A}={F}\left(1\right)\right)\right)$
12 11 rspccva ${⊢}\left(\forall {s}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\left(0{H}{s}={F}\left(0\right)\wedge 1{H}{s}={F}\left(1\right)\right)\wedge {A}\in \left[0,1\right]\right)\to \left(0{H}{A}={F}\left(0\right)\wedge 1{H}{A}={F}\left(1\right)\right)$
13 6 12 sylan ${⊢}\left({\phi }\wedge {A}\in \left[0,1\right]\right)\to \left(0{H}{A}={F}\left(0\right)\wedge 1{H}{A}={F}\left(1\right)\right)$