Metamath Proof Explorer

Theorem htpyi

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

		Ref	Expression
	Hypotheses	ishtpy.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
		ishtpy.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
		ishtpy.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
		htpyi.1	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
	Assertion	htpyi	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐻 0 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐴 𝐻 1 ) = ( 𝐺 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ishtpy.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		ishtpy.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3		ishtpy.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
4		htpyi.1	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
5	1 2 3	ishtpy	⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ↔ ( 𝐻 ∈ ( ( 𝐽 ×_t II ) Cn 𝐾 ) ∧ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) ) )
6	4 5	mpbid	⊢ ( 𝜑 → ( 𝐻 ∈ ( ( 𝐽 ×_t II ) Cn 𝐾 ) ∧ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) )
7	6	simprd	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) )
8		oveq1	⊢ ( 𝑠 = 𝐴 → ( 𝑠 𝐻 0 ) = ( 𝐴 𝐻 0 ) )
9		fveq2	⊢ ( 𝑠 = 𝐴 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝐴 ) )
10	8 9	eqeq12d	⊢ ( 𝑠 = 𝐴 → ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ↔ ( 𝐴 𝐻 0 ) = ( 𝐹 ‘ 𝐴 ) ) )
11		oveq1	⊢ ( 𝑠 = 𝐴 → ( 𝑠 𝐻 1 ) = ( 𝐴 𝐻 1 ) )
12		fveq2	⊢ ( 𝑠 = 𝐴 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝐴 ) )
13	11 12	eqeq12d	⊢ ( 𝑠 = 𝐴 → ( ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ↔ ( 𝐴 𝐻 1 ) = ( 𝐺 ‘ 𝐴 ) ) )
14	10 13	anbi12d	⊢ ( 𝑠 = 𝐴 → ( ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ↔ ( ( 𝐴 𝐻 0 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐴 𝐻 1 ) = ( 𝐺 ‘ 𝐴 ) ) ) )
15	14	rspccva	⊢ ( ( ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐻 0 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐴 𝐻 1 ) = ( 𝐺 ‘ 𝐴 ) ) )
16	7 15	sylan	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐻 0 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐴 𝐻 1 ) = ( 𝐺 ‘ 𝐴 ) ) )