Metamath Proof Explorer

Theorem phtpcer

Description: Path homotopy is an equivalence relation. Proposition 1.2 of Hatcher p. 26. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 6-Jul-2015) (Proof shortened by AV, 1-May-2021)

Ref Expression
Assertion phtpcer 
|- ( ~=ph ` J ) Er ( II Cn J )

Proof

Step Hyp Ref Expression
1 phtpcrel 
 |-  Rel ( ~=ph ` J )
2 isphtpc 
 |-  ( x ( ~=ph ` J ) y <-> ( x e. ( II Cn J ) /\ y e. ( II Cn J ) /\ ( x ( PHtpy ` J ) y ) =/= (/) ) )
3 2 simp2bi 
 |-  ( x ( ~=ph ` J ) y -> y e. ( II Cn J ) )
4 2 simp1bi 
 |-  ( x ( ~=ph ` J ) y -> x e. ( II Cn J ) )
5 2 simp3bi 
 |-  ( x ( ~=ph ` J ) y -> ( x ( PHtpy ` J ) y ) =/= (/) )
6 n0 
 |-  ( ( x ( PHtpy ` J ) y ) =/= (/) <-> E. f f e. ( x ( PHtpy ` J ) y ) )
7 5 6 sylib 
 |-  ( x ( ~=ph ` J ) y -> E. f f e. ( x ( PHtpy ` J ) y ) )
8 4 adantr 
 |-  ( ( x ( ~=ph ` J ) y /\ f e. ( x ( PHtpy ` J ) y ) ) -> x e. ( II Cn J ) )
9 3 adantr 
 |-  ( ( x ( ~=ph ` J ) y /\ f e. ( x ( PHtpy ` J ) y ) ) -> y e. ( II Cn J ) )
10 eqid 
 |-  ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( u f ( 1 - v ) ) ) = ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( u f ( 1 - v ) ) )
11 simpr 
 |-  ( ( x ( ~=ph ` J ) y /\ f e. ( x ( PHtpy ` J ) y ) ) -> f e. ( x ( PHtpy ` J ) y ) )
12 8 9 10 11 phtpycom 
 |-  ( ( x ( ~=ph ` J ) y /\ f e. ( x ( PHtpy ` J ) y ) ) -> ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( u f ( 1 - v ) ) ) e. ( y ( PHtpy ` J ) x ) )
13 12 ne0d 
 |-  ( ( x ( ~=ph ` J ) y /\ f e. ( x ( PHtpy ` J ) y ) ) -> ( y ( PHtpy ` J ) x ) =/= (/) )
14 7 13 exlimddv 
 |-  ( x ( ~=ph ` J ) y -> ( y ( PHtpy ` J ) x ) =/= (/) )
15 isphtpc 
 |-  ( y ( ~=ph ` J ) x <-> ( y e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( y ( PHtpy ` J ) x ) =/= (/) ) )
16 3 4 14 15 syl3anbrc 
 |-  ( x ( ~=ph ` J ) y -> y ( ~=ph ` J ) x )
17 4 adantr 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> x e. ( II Cn J ) )
18 simpr 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> y ( ~=ph ` J ) z )
19 isphtpc 
 |-  ( y ( ~=ph ` J ) z <-> ( y e. ( II Cn J ) /\ z e. ( II Cn J ) /\ ( y ( PHtpy ` J ) z ) =/= (/) ) )
20 18 19 sylib 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> ( y e. ( II Cn J ) /\ z e. ( II Cn J ) /\ ( y ( PHtpy ` J ) z ) =/= (/) ) )
21 20 simp2d 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> z e. ( II Cn J ) )
22 5 adantr 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> ( x ( PHtpy ` J ) y ) =/= (/) )
23 22 6 sylib 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> E. f f e. ( x ( PHtpy ` J ) y ) )
24 20 simp3d 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> ( y ( PHtpy ` J ) z ) =/= (/) )
25 n0 
 |-  ( ( y ( PHtpy ` J ) z ) =/= (/) <-> E. g g e. ( y ( PHtpy ` J ) z ) )
26 24 25 sylib 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> E. g g e. ( y ( PHtpy ` J ) z ) )
27 exdistrv 
 |-  ( E. f E. g ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) <-> ( E. f f e. ( x ( PHtpy ` J ) y ) /\ E. g g e. ( y ( PHtpy ` J ) z ) ) )
28 23 26 27 sylanbrc 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> E. f E. g ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) )
29 eqid 
 |-  ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> if ( v <_ ( 1 / 2 ) , ( u f ( 2 x. v ) ) , ( u g ( ( 2 x. v ) - 1 ) ) ) ) = ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> if ( v <_ ( 1 / 2 ) , ( u f ( 2 x. v ) ) , ( u g ( ( 2 x. v ) - 1 ) ) ) )
30 17 adantr 
 |-  ( ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) /\ ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) ) -> x e. ( II Cn J ) )
31 20 simp1d 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> y e. ( II Cn J ) )
32 31 adantr 
 |-  ( ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) /\ ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) ) -> y e. ( II Cn J ) )
33 21 adantr 
 |-  ( ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) /\ ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) ) -> z e. ( II Cn J ) )
34 simprl 
 |-  ( ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) /\ ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) ) -> f e. ( x ( PHtpy ` J ) y ) )
35 simprr 
 |-  ( ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) /\ ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) ) -> g e. ( y ( PHtpy ` J ) z ) )
36 29 30 32 33 34 35 phtpycc 
 |-  ( ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) /\ ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) ) -> ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> if ( v <_ ( 1 / 2 ) , ( u f ( 2 x. v ) ) , ( u g ( ( 2 x. v ) - 1 ) ) ) ) e. ( x ( PHtpy ` J ) z ) )
37 36 ne0d 
 |-  ( ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) /\ ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) ) -> ( x ( PHtpy ` J ) z ) =/= (/) )
38 37 ex 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> ( ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) -> ( x ( PHtpy ` J ) z ) =/= (/) ) )
39 38 exlimdvv 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> ( E. f E. g ( f e. ( x ( PHtpy ` J ) y ) /\ g e. ( y ( PHtpy ` J ) z ) ) -> ( x ( PHtpy ` J ) z ) =/= (/) ) )
40 28 39 mpd 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> ( x ( PHtpy ` J ) z ) =/= (/) )
41 isphtpc 
 |-  ( x ( ~=ph ` J ) z <-> ( x e. ( II Cn J ) /\ z e. ( II Cn J ) /\ ( x ( PHtpy ` J ) z ) =/= (/) ) )
42 17 21 40 41 syl3anbrc 
 |-  ( ( x ( ~=ph ` J ) y /\ y ( ~=ph ` J ) z ) -> x ( ~=ph ` J ) z )
43 eqid 
 |-  ( y e. ( 0 [,] 1 ) , z e. ( 0 [,] 1 ) |-> ( x ` y ) ) = ( y e. ( 0 [,] 1 ) , z e. ( 0 [,] 1 ) |-> ( x ` y ) )
44 id 
 |-  ( x e. ( II Cn J ) -> x e. ( II Cn J ) )
45 43 44 phtpyid 
 |-  ( x e. ( II Cn J ) -> ( y e. ( 0 [,] 1 ) , z e. ( 0 [,] 1 ) |-> ( x ` y ) ) e. ( x ( PHtpy ` J ) x ) )
46 45 ne0d 
 |-  ( x e. ( II Cn J ) -> ( x ( PHtpy ` J ) x ) =/= (/) )
47 46 ancli 
 |-  ( x e. ( II Cn J ) -> ( x e. ( II Cn J ) /\ ( x ( PHtpy ` J ) x ) =/= (/) ) )
48 47 pm4.71ri 
 |-  ( x e. ( II Cn J ) <-> ( ( x e. ( II Cn J ) /\ ( x ( PHtpy ` J ) x ) =/= (/) ) /\ x e. ( II Cn J ) ) )
49 df-3an 
 |-  ( ( x e. ( II Cn J ) /\ ( x ( PHtpy ` J ) x ) =/= (/) /\ x e. ( II Cn J ) ) <-> ( ( x e. ( II Cn J ) /\ ( x ( PHtpy ` J ) x ) =/= (/) ) /\ x e. ( II Cn J ) ) )
50 3ancomb 
 |-  ( ( x e. ( II Cn J ) /\ ( x ( PHtpy ` J ) x ) =/= (/) /\ x e. ( II Cn J ) ) <-> ( x e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( x ( PHtpy ` J ) x ) =/= (/) ) )
51 48 49 50 3bitr2i 
 |-  ( x e. ( II Cn J ) <-> ( x e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( x ( PHtpy ` J ) x ) =/= (/) ) )
52 isphtpc 
 |-  ( x ( ~=ph ` J ) x <-> ( x e. ( II Cn J ) /\ x e. ( II Cn J ) /\ ( x ( PHtpy ` J ) x ) =/= (/) ) )
53 51 52 bitr4i 
 |-  ( x e. ( II Cn J ) <-> x ( ~=ph ` J ) x )
54 1 16 42 53 iseri 
 |-  ( ~=ph ` J ) Er ( II Cn J )