Metamath Proof Explorer

Theorem htpyi

Description: A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015)

Ref Expression
Hypotheses ishtpy.1 ⊢ φ → J ∈ TopOn ⁡ X
ishtpy.3 ⊢ φ → F ∈ J Cn K
ishtpy.4 ⊢ φ → G ∈ J Cn K
htpyi.1 ⊢ φ → H ∈ F J Htpy K G
Assertion htpyi ⊢ φ ∧ A ∈ X → A H 0 = F ⁡ A ∧ A H 1 = G ⁡ A

Proof

Step Hyp Ref Expression
1 ishtpy.1 ⊢ φ → J ∈ TopOn ⁡ X
2 ishtpy.3 ⊢ φ → F ∈ J Cn K
3 ishtpy.4 ⊢ φ → G ∈ J Cn K
4 htpyi.1 ⊢ φ → H ∈ F J Htpy K G
5 1 2 3 ishtpy ⊢ φ → H ∈ F J Htpy K G ↔ H ∈ J × t II Cn K ∧ ∀ s ∈ X s H 0 = F ⁡ s ∧ s H 1 = G ⁡ s
6 4 5 mpbid ⊢ φ → H ∈ J × t II Cn K ∧ ∀ s ∈ X s H 0 = F ⁡ s ∧ s H 1 = G ⁡ s
7 6 simprd ⊢ φ → ∀ s ∈ X s H 0 = F ⁡ s ∧ s H 1 = G ⁡ s
8 oveq1 ⊢ s = A → s H 0 = A H 0
9 fveq2 ⊢ s = A → F ⁡ s = F ⁡ A
10 8 9 eqeq12d ⊢ s = A → s H 0 = F ⁡ s ↔ A H 0 = F ⁡ A
11 oveq1 ⊢ s = A → s H 1 = A H 1
12 fveq2 ⊢ s = A → G ⁡ s = G ⁡ A
13 11 12 eqeq12d ⊢ s = A → s H 1 = G ⁡ s ↔ A H 1 = G ⁡ A
14 10 13 anbi12d ⊢ s = A → s H 0 = F ⁡ s ∧ s H 1 = G ⁡ s ↔ A H 0 = F ⁡ A ∧ A H 1 = G ⁡ A
15 14 rspccva ⊢ ∀ s ∈ X s H 0 = F ⁡ s ∧ s H 1 = G ⁡ s ∧ A ∈ X → A H 0 = F ⁡ A ∧ A H 1 = G ⁡ A
16 7 15 sylan ⊢ φ ∧ A ∈ X → A H 0 = F ⁡ A ∧ A H 1 = G ⁡ A