Theorem sconnpht

Description: A closed path in a simply connected space is contractible to a point. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	sconnpht	⊢ ( ( 𝐽 ∈ SConn ∧ 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) ) → 𝐹 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		issconn	⊢ ( 𝐽 ∈ SConn ↔ ( 𝐽 ∈ PConn ∧ ∀ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ) )
2		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
3		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
4	2 3	eqeq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ↔ ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) ) )
5		id	⊢ ( 𝑓 = 𝐹 → 𝑓 = 𝐹 )
6	2	sneqd	⊢ ( 𝑓 = 𝐹 → { ( 𝑓 ‘ 0 ) } = { ( 𝐹 ‘ 0 ) } )
7	6	xpeq2d	⊢ ( 𝑓 = 𝐹 → ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )
8	5 7	breq12d	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ↔ 𝐹 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) )
9	4 8	imbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ↔ ( ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) → 𝐹 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) ) )
10	9	rspccv	⊢ ( ∀ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) → ( 𝐹 ∈ ( II Cn 𝐽 ) → ( ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) → 𝐹 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) ) )
11	1 10	simplbiim	⊢ ( 𝐽 ∈ SConn → ( 𝐹 ∈ ( II Cn 𝐽 ) → ( ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) → 𝐹 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ) ) )
12	11	3imp	⊢ ( ( 𝐽 ∈ SConn ∧ 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 0 ) = ( 𝐹 ‘ 1 ) ) → 𝐹 ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )