Metamath Proof Explorer

Theorem pi1cof

Description: Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses pi1co.p 
|- P = ( J pi1 A )
pi1co.q 
|- Q = ( K pi1 B )
pi1co.v 
|- V = ( Base ` P )
pi1co.g 
|- G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )
pi1co.j 
|- ( ph -> J e. ( TopOn ` X ) )
pi1co.f 
|- ( ph -> F e. ( J Cn K ) )
pi1co.a 
|- ( ph -> A e. X )
pi1co.b 
|- ( ph -> ( F ` A ) = B )
Assertion pi1cof 
|- ( ph -> G : V --> ( Base ` Q ) )

Proof

Step Hyp Ref Expression
1 pi1co.p 
 |-  P = ( J pi1 A )
2 pi1co.q 
 |-  Q = ( K pi1 B )
3 pi1co.v 
 |-  V = ( Base ` P )
4 pi1co.g 
 |-  G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )
5 pi1co.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
6 pi1co.f 
 |-  ( ph -> F e. ( J Cn K ) )
7 pi1co.a 
 |-  ( ph -> A e. X )
8 pi1co.b 
 |-  ( ph -> ( F ` A ) = B )
9 fvex 
 |-  ( ~=ph ` J ) e. _V
10 ecexg 
 |-  ( ( ~=ph ` J ) e. _V -> [ g ] ( ~=ph ` J ) e. _V )
11 9 10 mp1i 
 |-  ( ( ph /\ g e. U. V ) -> [ g ] ( ~=ph ` J ) e. _V )
12 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
13 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
14 6 13 syl 
 |-  ( ph -> K e. Top )
15 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
16 14 15 sylib 
 |-  ( ph -> K e. ( TopOn ` U. K ) )
17 16 adantr 
 |-  ( ( ph /\ g e. U. V ) -> K e. ( TopOn ` U. K ) )
18 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) /\ F e. ( J Cn K ) ) -> F : X --> U. K )
19 5 16 6 18 syl3anc 
 |-  ( ph -> F : X --> U. K )
20 19 7 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. U. K )
21 8 20 eqeltrrd 
 |-  ( ph -> B e. U. K )
22 21 adantr 
 |-  ( ( ph /\ g e. U. V ) -> B e. U. K )
23 3 a1i 
 |-  ( ph -> V = ( Base ` P ) )
24 1 5 7 23 pi1eluni 
 |-  ( ph -> ( g e. U. V <-> ( g e. ( II Cn J ) /\ ( g ` 0 ) = A /\ ( g ` 1 ) = A ) ) )
25 24 biimpa 
 |-  ( ( ph /\ g e. U. V ) -> ( g e. ( II Cn J ) /\ ( g ` 0 ) = A /\ ( g ` 1 ) = A ) )
26 25 simp1d 
 |-  ( ( ph /\ g e. U. V ) -> g e. ( II Cn J ) )
27 6 adantr 
 |-  ( ( ph /\ g e. U. V ) -> F e. ( J Cn K ) )
28 cnco 
 |-  ( ( g e. ( II Cn J ) /\ F e. ( J Cn K ) ) -> ( F o. g ) e. ( II Cn K ) )
29 26 27 28 syl2anc 
 |-  ( ( ph /\ g e. U. V ) -> ( F o. g ) e. ( II Cn K ) )
30 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
31 cnf2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` X ) /\ g e. ( II Cn J ) ) -> g : ( 0 [,] 1 ) --> X )
32 30 5 26 31 mp3an2ani 
 |-  ( ( ph /\ g e. U. V ) -> g : ( 0 [,] 1 ) --> X )
33 0elunit 
 |-  0 e. ( 0 [,] 1 )
34 fvco3 
 |-  ( ( g : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( ( F o. g ) ` 0 ) = ( F ` ( g ` 0 ) ) )
35 32 33 34 sylancl 
 |-  ( ( ph /\ g e. U. V ) -> ( ( F o. g ) ` 0 ) = ( F ` ( g ` 0 ) ) )
36 25 simp2d 
 |-  ( ( ph /\ g e. U. V ) -> ( g ` 0 ) = A )
37 36 fveq2d 
 |-  ( ( ph /\ g e. U. V ) -> ( F ` ( g ` 0 ) ) = ( F ` A ) )
38 8 adantr 
 |-  ( ( ph /\ g e. U. V ) -> ( F ` A ) = B )
39 35 37 38 3eqtrd 
 |-  ( ( ph /\ g e. U. V ) -> ( ( F o. g ) ` 0 ) = B )
40 1elunit 
 |-  1 e. ( 0 [,] 1 )
41 fvco3 
 |-  ( ( g : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. g ) ` 1 ) = ( F ` ( g ` 1 ) ) )
42 32 40 41 sylancl 
 |-  ( ( ph /\ g e. U. V ) -> ( ( F o. g ) ` 1 ) = ( F ` ( g ` 1 ) ) )
43 25 simp3d 
 |-  ( ( ph /\ g e. U. V ) -> ( g ` 1 ) = A )
44 43 fveq2d 
 |-  ( ( ph /\ g e. U. V ) -> ( F ` ( g ` 1 ) ) = ( F ` A ) )
45 42 44 38 3eqtrd 
 |-  ( ( ph /\ g e. U. V ) -> ( ( F o. g ) ` 1 ) = B )
46 2 12 17 22 29 39 45 elpi1i 
 |-  ( ( ph /\ g e. U. V ) -> [ ( F o. g ) ] ( ~=ph ` K ) e. ( Base ` Q ) )
47 eceq1 
 |-  ( g = h -> [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) )
48 coeq2 
 |-  ( g = h -> ( F o. g ) = ( F o. h ) )
49 48 eceq1d 
 |-  ( g = h -> [ ( F o. g ) ] ( ~=ph ` K ) = [ ( F o. h ) ] ( ~=ph ` K ) )
50 phtpcer 
 |-  ( ~=ph ` K ) Er ( II Cn K )
51 50 a1i 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( ~=ph ` K ) Er ( II Cn K ) )
52 simpr3 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) )
53 phtpcer 
 |-  ( ~=ph ` J ) Er ( II Cn J )
54 53 a1i 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( ~=ph ` J ) Er ( II Cn J ) )
55 simpr1 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> g e. U. V )
56 24 adantr 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( g e. U. V <-> ( g e. ( II Cn J ) /\ ( g ` 0 ) = A /\ ( g ` 1 ) = A ) ) )
57 55 56 mpbid 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( g e. ( II Cn J ) /\ ( g ` 0 ) = A /\ ( g ` 1 ) = A ) )
58 57 simp1d 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> g e. ( II Cn J ) )
59 54 58 erth 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( g ( ~=ph ` J ) h <-> [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) )
60 52 59 mpbird 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> g ( ~=ph ` J ) h )
61 6 adantr 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> F e. ( J Cn K ) )
62 60 61 phtpcco2 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( F o. g ) ( ~=ph ` K ) ( F o. h ) )
63 51 62 erthi 
 |-  ( ( ph /\ ( g e. U. V /\ h e. U. V /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> [ ( F o. g ) ] ( ~=ph ` K ) = [ ( F o. h ) ] ( ~=ph ` K ) )
64 4 11 46 47 49 63 fliftfund 
 |-  ( ph -> Fun G )
65 4 11 46 fliftf 
 |-  ( ph -> ( Fun G <-> G : ran ( g e. U. V |-> [ g ] ( ~=ph ` J ) ) --> ( Base ` Q ) ) )
66 64 65 mpbid 
 |-  ( ph -> G : ran ( g e. U. V |-> [ g ] ( ~=ph ` J ) ) --> ( Base ` Q ) )
67 1 5 7 23 pi1bas2 
 |-  ( ph -> V = ( U. V /. ( ~=ph ` J ) ) )
68 df-qs 
 |-  ( U. V /. ( ~=ph ` J ) ) = { s | E. g e. U. V s = [ g ] ( ~=ph ` J ) }
69 eqid 
 |-  ( g e. U. V |-> [ g ] ( ~=ph ` J ) ) = ( g e. U. V |-> [ g ] ( ~=ph ` J ) )
70 69 rnmpt 
 |-  ran ( g e. U. V |-> [ g ] ( ~=ph ` J ) ) = { s | E. g e. U. V s = [ g ] ( ~=ph ` J ) }
71 68 70 eqtr4i 
 |-  ( U. V /. ( ~=ph ` J ) ) = ran ( g e. U. V |-> [ g ] ( ~=ph ` J ) )
72 67 71 eqtrdi 
 |-  ( ph -> V = ran ( g e. U. V |-> [ g ] ( ~=ph ` J ) ) )
73 72 feq2d 
 |-  ( ph -> ( G : V --> ( Base ` Q ) <-> G : ran ( g e. U. V |-> [ g ] ( ~=ph ` J ) ) --> ( Base ` Q ) ) )
74 66 73 mpbird 
 |-  ( ph -> G : V --> ( Base ` Q ) )