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 ∈ II Cn J
isphtpy.3 ⊢ φ → G ∈ II Cn J
phtpyi.1 ⊢ φ → H ∈ F PHtpy ⁡ J G
Assertion phtpyi ⊢ φ ∧ A ∈ 0 1 → 0 H A = F ⁡ 0 ∧ 1 H A = F ⁡ 1

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢ φ → F ∈ II Cn J
2 isphtpy.3 ⊢ φ → G ∈ II Cn J
3 phtpyi.1 ⊢ φ → H ∈ F PHtpy ⁡ J G
4 1 2 isphtpy ⊢ φ → H ∈ F PHtpy ⁡ J G ↔ H ∈ F II Htpy J G ∧ ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
5 3 4 mpbid ⊢ φ → H ∈ F II Htpy J G ∧ ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
6 5 simprd ⊢ φ → ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
7 oveq2 ⊢ s = A → 0 H s = 0 H A
8 7 eqeq1d ⊢ s = A → 0 H s = F ⁡ 0 ↔ 0 H A = F ⁡ 0
9 oveq2 ⊢ s = A → 1 H s = 1 H A
10 9 eqeq1d ⊢ s = A → 1 H s = F ⁡ 1 ↔ 1 H A = F ⁡ 1
11 8 10 anbi12d ⊢ s = A → 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1 ↔ 0 H A = F ⁡ 0 ∧ 1 H A = F ⁡ 1
12 11 rspccva ⊢ ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1 ∧ A ∈ 0 1 → 0 H A = F ⁡ 0 ∧ 1 H A = F ⁡ 1
13 6 12 sylan ⊢ φ ∧ A ∈ 0 1 → 0 H A = F ⁡ 0 ∧ 1 H A = F ⁡ 1