Metamath Proof Explorer

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 
|- ( ( J e. SConn /\ F e. ( II Cn J ) /\ ( F ` 0 ) = ( F ` 1 ) ) -> F ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )

Proof

Step Hyp Ref Expression
1 issconn 
 |-  ( J e. SConn <-> ( J e. PConn /\ A. f e. ( II Cn J ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) ) )
2 fveq1 
 |-  ( f = F -> ( f ` 0 ) = ( F ` 0 ) )
3 fveq1 
 |-  ( f = F -> ( f ` 1 ) = ( F ` 1 ) )
4 2 3 eqeq12d 
 |-  ( f = F -> ( ( f ` 0 ) = ( f ` 1 ) <-> ( F ` 0 ) = ( F ` 1 ) ) )
5 id 
 |-  ( f = F -> f = F )
6 2 sneqd 
 |-  ( f = F -> { ( f ` 0 ) } = { ( F ` 0 ) } )
7 6 xpeq2d 
 |-  ( f = F -> ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
8 5 7 breq12d 
 |-  ( f = F -> ( f ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) <-> F ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ) )
9 4 8 imbi12d 
 |-  ( f = F -> ( ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) <-> ( ( F ` 0 ) = ( F ` 1 ) -> F ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ) ) )
10 9 rspccv 
 |-  ( A. f e. ( II Cn J ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) -> ( F e. ( II Cn J ) -> ( ( F ` 0 ) = ( F ` 1 ) -> F ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ) ) )
11 1 10 simplbiim 
 |-  ( J e. SConn -> ( F e. ( II Cn J ) -> ( ( F ` 0 ) = ( F ` 1 ) -> F ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ) ) )
12 11 3imp 
 |-  ( ( J e. SConn /\ F e. ( II Cn J ) /\ ( F ` 0 ) = ( F ` 1 ) ) -> F ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )