# Metamath Proof Explorer

## Theorem htpyi

Description: A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-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)$
htpyi.1 ${⊢}{\phi }\to {H}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){G}\right)$
Assertion htpyi ${⊢}\left({\phi }\wedge {A}\in {X}\right)\to \left({A}{H}0={F}\left({A}\right)\wedge {A}{H}1={G}\left({A}\right)\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 htpyi.1 ${⊢}{\phi }\to {H}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){G}\right)$
5 1 2 3 ishtpy ${⊢}{\phi }\to \left({H}\in \left({F}\left({J}\mathrm{Htpy}{K}\right){G}\right)↔\left({H}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)\wedge \forall {s}\in {X}\phantom{\rule{.4em}{0ex}}\left({s}{H}0={F}\left({s}\right)\wedge {s}{H}1={G}\left({s}\right)\right)\right)\right)$
6 4 5 mpbid ${⊢}{\phi }\to \left({H}\in \left(\left({J}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{K}\right)\wedge \forall {s}\in {X}\phantom{\rule{.4em}{0ex}}\left({s}{H}0={F}\left({s}\right)\wedge {s}{H}1={G}\left({s}\right)\right)\right)$
7 6 simprd ${⊢}{\phi }\to \forall {s}\in {X}\phantom{\rule{.4em}{0ex}}\left({s}{H}0={F}\left({s}\right)\wedge {s}{H}1={G}\left({s}\right)\right)$
8 oveq1 ${⊢}{s}={A}\to {s}{H}0={A}{H}0$
9 fveq2 ${⊢}{s}={A}\to {F}\left({s}\right)={F}\left({A}\right)$
10 8 9 eqeq12d ${⊢}{s}={A}\to \left({s}{H}0={F}\left({s}\right)↔{A}{H}0={F}\left({A}\right)\right)$
11 oveq1 ${⊢}{s}={A}\to {s}{H}1={A}{H}1$
12 fveq2 ${⊢}{s}={A}\to {G}\left({s}\right)={G}\left({A}\right)$
13 11 12 eqeq12d ${⊢}{s}={A}\to \left({s}{H}1={G}\left({s}\right)↔{A}{H}1={G}\left({A}\right)\right)$
14 10 13 anbi12d ${⊢}{s}={A}\to \left(\left({s}{H}0={F}\left({s}\right)\wedge {s}{H}1={G}\left({s}\right)\right)↔\left({A}{H}0={F}\left({A}\right)\wedge {A}{H}1={G}\left({A}\right)\right)\right)$
15 14 rspccva ${⊢}\left(\forall {s}\in {X}\phantom{\rule{.4em}{0ex}}\left({s}{H}0={F}\left({s}\right)\wedge {s}{H}1={G}\left({s}\right)\right)\wedge {A}\in {X}\right)\to \left({A}{H}0={F}\left({A}\right)\wedge {A}{H}1={G}\left({A}\right)\right)$
16 7 15 sylan ${⊢}\left({\phi }\wedge {A}\in {X}\right)\to \left({A}{H}0={F}\left({A}\right)\wedge {A}{H}1={G}\left({A}\right)\right)$