Metamath Proof Explorer

Theorem sconnpht2

Description: Any two paths in a simply connected space with the same start and end point are path-homotopic. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses sconnpht2.1 ⊢ ( 𝜑 → 𝐽 ∈ SConn )
sconnpht2.2 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
sconnpht2.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
sconnpht2.4 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) )
sconnpht2.5 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
Assertion sconnpht2 ( 𝜑 → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 sconnpht2.1 ⊢ ( 𝜑 → 𝐽 ∈ SConn )
2 sconnpht2.2 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
3 sconnpht2.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
4 sconnpht2.4 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) )
5 sconnpht2.5 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
6 eqid ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) )
7 6 pcorevcl ⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ‘ 0 ) = ( 𝐺 ‘ 1 ) ∧ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ‘ 1 ) = ( 𝐺 ‘ 0 ) ) )
8 3 7 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ‘ 0 ) = ( 𝐺 ‘ 1 ) ∧ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ‘ 1 ) = ( 𝐺 ‘ 0 ) ) )
9 8 simp1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ∈ ( II Cn 𝐽 ) )
10 8 simp2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ‘ 0 ) = ( 𝐺 ‘ 1 ) )
11 5 10 eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ‘ 0 ) )
12 2 9 11 pcocn ⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ∈ ( II Cn 𝐽 ) )
13 2 9 pco0 ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 0 ) = ( 𝐹 ‘ 0 ) )
14 2 9 pco1 ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 1 ) = ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ‘ 1 ) )
15 8 simp3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ‘ 1 ) = ( 𝐺 ‘ 0 ) )
16 4 15 eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ‘ 1 ) )
17 14 16 eqtr4d ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 1 ) = ( 𝐹 ‘ 0 ) )
18 13 17 eqtr4d ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 0 ) = ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 1 ) )
19 sconnpht ⊢ ( ( 𝐽 ∈ SConn ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 0 ) = ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 1 ) ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 0 ) } ) )
20 1 12 18 19 syl3anc ⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 0 ) } ) )
21 13 sneqd ⊢ ( 𝜑 → { ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 0 ) } = { ( 𝐹 ‘ 0 ) } )
22 21 xpeq2d ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ‘ 0 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )
23 20 22 breqtrd ⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) )
24 eqid ⊢ ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } )
25 6 24 2 3 4 5 pcophtb ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) ) ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) ↔ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) )
26 23 25 mpbid ⊢ ( 𝜑 → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 )