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 
|- H = ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) )
pcophtb.p 
|- P = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } )
pcophtb.f 
|- ( ph -> F e. ( II Cn J ) )
pcophtb.g 
|- ( ph -> G e. ( II Cn J ) )
pcophtb.0 
|- ( ph -> ( F ` 0 ) = ( G ` 0 ) )
pcophtb.1 
|- ( ph -> ( F ` 1 ) = ( G ` 1 ) )
Assertion pcophtb 
|- ( ph -> ( ( F ( *p ` J ) H ) ( ~=ph ` J ) P <-> F ( ~=ph ` J ) G ) )

Proof

Step Hyp Ref Expression
1 pcophtb.h 
 |-  H = ( x e. ( 0 [,] 1 ) |-> ( G ` ( 1 - x ) ) )
2 pcophtb.p 
 |-  P = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } )
3 pcophtb.f 
 |-  ( ph -> F e. ( II Cn J ) )
4 pcophtb.g 
 |-  ( ph -> G e. ( II Cn J ) )
5 pcophtb.0 
 |-  ( ph -> ( F ` 0 ) = ( G ` 0 ) )
6 pcophtb.1 
 |-  ( ph -> ( F ` 1 ) = ( G ` 1 ) )
7 phtpcer 
 |-  ( ~=ph ` J ) Er ( II Cn J )
8 7 a1i 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( ~=ph ` J ) Er ( II Cn J ) )
9 1 pcorevcl 
 |-  ( G e. ( II Cn J ) -> ( H e. ( II Cn J ) /\ ( H ` 0 ) = ( G ` 1 ) /\ ( H ` 1 ) = ( G ` 0 ) ) )
10 4 9 syl 
 |-  ( ph -> ( H e. ( II Cn J ) /\ ( H ` 0 ) = ( G ` 1 ) /\ ( H ` 1 ) = ( G ` 0 ) ) )
11 10 simp2d 
 |-  ( ph -> ( H ` 0 ) = ( G ` 1 ) )
12 6 11 eqtr4d 
 |-  ( ph -> ( F ` 1 ) = ( H ` 0 ) )
13 10 simp1d 
 |-  ( ph -> H e. ( II Cn J ) )
14 13 4 pco0 
 |-  ( ph -> ( ( H ( *p ` J ) G ) ` 0 ) = ( H ` 0 ) )
15 12 14 eqtr4d 
 |-  ( ph -> ( F ` 1 ) = ( ( H ( *p ` J ) G ) ` 0 ) )
16 15 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ` 1 ) = ( ( H ( *p ` J ) G ) ` 0 ) )
17 3 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> F e. ( II Cn J ) )
18 8 17 erref 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> F ( ~=ph ` J ) F )
19 eqid 
 |-  ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) = ( ( 0 [,] 1 ) X. { ( G ` 1 ) } )
20 1 19 pcorev 
 |-  ( G e. ( II Cn J ) -> ( H ( *p ` J ) G ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) )
21 4 20 syl 
 |-  ( ph -> ( H ( *p ` J ) G ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) )
22 21 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( H ( *p ` J ) G ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) )
23 16 18 22 pcohtpy 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ( *p ` J ) ( H ( *p ` J ) G ) ) ( ~=ph ` J ) ( F ( *p ` J ) ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) ) )
24 6 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ` 1 ) = ( G ` 1 ) )
25 19 pcopt2 
 |-  ( ( F e. ( II Cn J ) /\ ( F ` 1 ) = ( G ` 1 ) ) -> ( F ( *p ` J ) ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) ) ( ~=ph ` J ) F )
26 17 24 25 syl2anc 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ( *p ` J ) ( ( 0 [,] 1 ) X. { ( G ` 1 ) } ) ) ( ~=ph ` J ) F )
27 8 23 26 ertrd 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ( *p ` J ) ( H ( *p ` J ) G ) ) ( ~=ph ` J ) F )
28 13 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> H e. ( II Cn J ) )
29 4 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> G e. ( II Cn J ) )
30 12 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ` 1 ) = ( H ` 0 ) )
31 10 simp3d 
 |-  ( ph -> ( H ` 1 ) = ( G ` 0 ) )
32 31 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( H ` 1 ) = ( G ` 0 ) )
33 eqid 
 |-  ( y e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) ) = ( y e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) )
34 17 28 29 30 32 33 pcoass 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( ( F ( *p ` J ) H ) ( *p ` J ) G ) ( ~=ph ` J ) ( F ( *p ` J ) ( H ( *p ` J ) G ) ) )
35 3 13 pco1 
 |-  ( ph -> ( ( F ( *p ` J ) H ) ` 1 ) = ( H ` 1 ) )
36 35 31 eqtrd 
 |-  ( ph -> ( ( F ( *p ` J ) H ) ` 1 ) = ( G ` 0 ) )
37 36 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( ( F ( *p ` J ) H ) ` 1 ) = ( G ` 0 ) )
38 simpr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ( *p ` J ) H ) ( ~=ph ` J ) P )
39 8 29 erref 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> G ( ~=ph ` J ) G )
40 37 38 39 pcohtpy 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( ( F ( *p ` J ) H ) ( *p ` J ) G ) ( ~=ph ` J ) ( P ( *p ` J ) G ) )
41 8 34 40 ertr3d 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ( *p ` J ) ( H ( *p ` J ) G ) ) ( ~=ph ` J ) ( P ( *p ` J ) G ) )
42 5 adantr 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ` 0 ) = ( G ` 0 ) )
43 42 eqcomd 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( G ` 0 ) = ( F ` 0 ) )
44 2 pcopt 
 |-  ( ( G e. ( II Cn J ) /\ ( G ` 0 ) = ( F ` 0 ) ) -> ( P ( *p ` J ) G ) ( ~=ph ` J ) G )
45 29 43 44 syl2anc 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( P ( *p ` J ) G ) ( ~=ph ` J ) G )
46 8 41 45 ertrd 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> ( F ( *p ` J ) ( H ( *p ` J ) G ) ) ( ~=ph ` J ) G )
47 8 27 46 ertr3d 
 |-  ( ( ph /\ ( F ( *p ` J ) H ) ( ~=ph ` J ) P ) -> F ( ~=ph ` J ) G )
48 7 a1i 
 |-  ( ( ph /\ F ( ~=ph ` J ) G ) -> ( ~=ph ` J ) Er ( II Cn J ) )
49 12 adantr 
 |-  ( ( ph /\ F ( ~=ph ` J ) G ) -> ( F ` 1 ) = ( H ` 0 ) )
50 simpr 
 |-  ( ( ph /\ F ( ~=ph ` J ) G ) -> F ( ~=ph ` J ) G )
51 13 adantr 
 |-  ( ( ph /\ F ( ~=ph ` J ) G ) -> H e. ( II Cn J ) )
52 48 51 erref 
 |-  ( ( ph /\ F ( ~=ph ` J ) G ) -> H ( ~=ph ` J ) H )
53 49 50 52 pcohtpy 
 |-  ( ( ph /\ F ( ~=ph ` J ) G ) -> ( F ( *p ` J ) H ) ( ~=ph ` J ) ( G ( *p ` J ) H ) )
54 eqid 
 |-  ( ( 0 [,] 1 ) X. { ( G ` 0 ) } ) = ( ( 0 [,] 1 ) X. { ( G ` 0 ) } )
55 1 54 pcorev2 
 |-  ( G e. ( II Cn J ) -> ( G ( *p ` J ) H ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( G ` 0 ) } ) )
56 4 55 syl 
 |-  ( ph -> ( G ( *p ` J ) H ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( G ` 0 ) } ) )
57 5 sneqd 
 |-  ( ph -> { ( F ` 0 ) } = { ( G ` 0 ) } )
58 57 xpeq2d 
 |-  ( ph -> ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) = ( ( 0 [,] 1 ) X. { ( G ` 0 ) } ) )
59 2 58 syl5eq 
 |-  ( ph -> P = ( ( 0 [,] 1 ) X. { ( G ` 0 ) } ) )
60 56 59 breqtrrd 
 |-  ( ph -> ( G ( *p ` J ) H ) ( ~=ph ` J ) P )
61 60 adantr 
 |-  ( ( ph /\ F ( ~=ph ` J ) G ) -> ( G ( *p ` J ) H ) ( ~=ph ` J ) P )
62 48 53 61 ertrd 
 |-  ( ( ph /\ F ( ~=ph ` J ) G ) -> ( F ( *p ` J ) H ) ( ~=ph ` J ) P )
63 47 62 impbida 
 |-  ( ph -> ( ( F ( *p ` J ) H ) ( ~=ph ` J ) P <-> F ( ~=ph ` J ) G ) )