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 ⊢φ→F∈IICnJ
isphtpy.3 ⊢φ→G∈IICnJ
phtpyi.1 ⊢φ→H∈FPHtpy⁡JG
Assertion phtpyi ⊢φ∧A∈01→0HA=F⁡0∧1HA=F⁡1

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢φ→F∈IICnJ
2 isphtpy.3 ⊢φ→G∈IICnJ
3 phtpyi.1 ⊢φ→H∈FPHtpy⁡JG
4 1 2 isphtpy ⊢φ→H∈FPHtpy⁡JG↔H∈FIIHtpyJG∧∀s∈010Hs=F⁡0∧1Hs=F⁡1
5 3 4 mpbid ⊢φ→H∈FIIHtpyJG∧∀s∈010Hs=F⁡0∧1Hs=F⁡1
6 5 simprd ⊢φ→∀s∈010Hs=F⁡0∧1Hs=F⁡1
7 oveq2 ⊢s=A→0Hs=0HA
8 7 eqeq1d ⊢s=A→0Hs=F⁡0↔0HA=F⁡0
9 oveq2 ⊢s=A→1Hs=1HA
10 9 eqeq1d ⊢s=A→1Hs=F⁡1↔1HA=F⁡1
11 8 10 anbi12d ⊢s=A→0Hs=F⁡0∧1Hs=F⁡1↔0HA=F⁡0∧1HA=F⁡1
12 11 rspccva ⊢∀s∈010Hs=F⁡0∧1Hs=F⁡1∧A∈01→0HA=F⁡0∧1HA=F⁡1
13 6 12 sylan ⊢φ∧A∈01→0HA=F⁡0∧1HA=F⁡1