Metamath Proof Explorer

Theorem pcophtb

Description: The path homotopy equivalence relation on two paths F , G with the same start and end point can be written in terms of the loop F - G formed by concatenating F with the inverse of G . Thus, all the homotopy information in ~=phJ is available if we restrict our attention to closed loops, as in the definition of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses pcophtb.h ⊢ 𝐻 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) )
pcophtb.p ⊢ 𝑃 = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } )
pcophtb.f ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
pcophtb.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
pcophtb.0 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) )
pcophtb.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
Assertion pcophtb ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ↔ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 pcophtb.h ⊢ 𝐻 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ ( 1 − 𝑥 ) ) )
2 pcophtb.p ⊢ 𝑃 = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } )
3 pcophtb.f ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
4 pcophtb.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
5 pcophtb.0 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) )
6 pcophtb.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
7 phtpcer ⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )
8 7 a1i ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
9 1 pcorevcl ⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → ( 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐻 ‘ 0 ) = ( 𝐺 ‘ 1 ) ∧ ( 𝐻 ‘ 1 ) = ( 𝐺 ‘ 0 ) ) )
10 4 9 syl ⊢ ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐻 ‘ 0 ) = ( 𝐺 ‘ 1 ) ∧ ( 𝐻 ‘ 1 ) = ( 𝐺 ‘ 0 ) ) )
11 10 simp2d ⊢ ( 𝜑 → ( 𝐻 ‘ 0 ) = ( 𝐺 ‘ 1 ) )
12 6 11 eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐻 ‘ 0 ) )
13 10 simp1d ⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐽 ) )
14 13 4 pco0 ⊢ ( 𝜑 → ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 0 ) = ( 𝐻 ‘ 0 ) )
15 12 14 eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 0 ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ‘ 1 ) = ( ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 0 ) )
17 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → 𝐹 ∈ ( II Cn 𝐽 ) )
18 8 17 erref ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐹 )
19 eqid ⊢ ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } )
20 1 19 pcorev ⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) )
21 4 20 syl ⊢ ( 𝜑 → ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) )
23 16 18 22 pcohtpy ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ) ( ≃ph ‘ 𝐽 ) ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) ) )
24 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
25 19 pcopt2 ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) ) ( ≃ph ‘ 𝐽 ) 𝐹 )
26 17 24 25 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 1 ) } ) ) ( ≃ph ‘ 𝐽 ) 𝐹 )
27 8 23 26 ertrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ) ( ≃ph ‘ 𝐽 ) 𝐹 )
28 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → 𝐻 ∈ ( II Cn 𝐽 ) )
29 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → 𝐺 ∈ ( II Cn 𝐽 ) )
30 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ‘ 1 ) = ( 𝐻 ‘ 0 ) )
31 10 simp3d ⊢ ( 𝜑 → ( 𝐻 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐻 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
33 eqid ⊢ ( 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) , ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) ) ) = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 ≤ ( 1 / 2 ) , if ( 𝑦 ≤ ( 1 / 4 ) , ( 2 · 𝑦 ) , ( 𝑦 + ( 1 / 4 ) ) ) , ( ( 𝑦 / 2 ) + ( 1 / 2 ) ) ) )
34 17 28 29 30 32 33 pcoass ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ) )
35 3 13 pco1 ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ‘ 1 ) = ( 𝐻 ‘ 1 ) )
36 35 31 eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ‘ 1 ) = ( 𝐺 ‘ 0 ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ‘ 1 ) = ( 𝐺 ‘ 0 ) )
38 simpr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 )
39 8 29 erref ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → 𝐺 ( ≃ph ‘ 𝐽 ) 𝐺 )
40 37 38 39 pcohtpy ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) ( 𝑃 ( *𝑝 ‘ 𝐽 ) 𝐺 ) )
41 8 34 40 ertr3d ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ) ( ≃ph ‘ 𝐽 ) ( 𝑃 ( *𝑝 ‘ 𝐽 ) 𝐺 ) )
42 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) )
43 42 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐺 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
44 2 pcopt ⊢ ( ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ‘ 0 ) = ( 𝐹 ‘ 0 ) ) → ( 𝑃 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) 𝐺 )
45 29 43 44 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝑃 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ( ≃ph ‘ 𝐽 ) 𝐺 )
46 8 41 45 ertrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝐻 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ) ( ≃ph ‘ 𝐽 ) 𝐺 )
47 8 27 46 ertr3d ⊢ ( ( 𝜑 ∧ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ) → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 )
48 7 a1i ⊢ ( ( 𝜑 ∧ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
49 12 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) → ( 𝐹 ‘ 1 ) = ( 𝐻 ‘ 0 ) )
50 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) → 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 )
51 13 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) → 𝐻 ∈ ( II Cn 𝐽 ) )
52 48 51 erref ⊢ ( ( 𝜑 ∧ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) → 𝐻 ( ≃ph ‘ 𝐽 ) 𝐻 )
53 49 50 52 pcohtpy ⊢ ( ( 𝜑 ∧ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐻 ) )
54 eqid ⊢ ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 0 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 0 ) } )
55 1 54 pcorev2 ⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 0 ) } ) )
56 4 55 syl ⊢ ( 𝜑 → ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 0 ) } ) )
57 5 sneqd ⊢ ( 𝜑 → { ( 𝐹 ‘ 0 ) } = { ( 𝐺 ‘ 0 ) } )
58 57 xpeq2d ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 0 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 0 ) } ) )
59 2 58 eqtrid ⊢ ( 𝜑 → 𝑃 = ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 0 ) } ) )
60 56 59 breqtrrd ⊢ ( 𝜑 → ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) → ( 𝐺 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 )
62 48 53 61 ertrd ⊢ ( ( 𝜑 ∧ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 )
63 47 62 impbida ⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐻 ) ( ≃ph ‘ 𝐽 ) 𝑃 ↔ 𝐹 ( ≃ph ‘ 𝐽 ) 𝐺 ) )