Metamath Proof Explorer

Theorem pi1xfrf

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

Ref Expression
Hypotheses pi1xfr.p 
|- P = ( J pi1 ( F ` 0 ) )
pi1xfr.q 
|- Q = ( J pi1 ( F ` 1 ) )
pi1xfr.b 
|- B = ( Base ` P )
pi1xfr.g 
|- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
pi1xfr.j 
|- ( ph -> J e. ( TopOn ` X ) )
pi1xfr.f 
|- ( ph -> F e. ( II Cn J ) )
pi1xfrval.i 
|- ( ph -> I e. ( II Cn J ) )
pi1xfrval.1 
|- ( ph -> ( F ` 1 ) = ( I ` 0 ) )
pi1xfrval.2 
|- ( ph -> ( I ` 1 ) = ( F ` 0 ) )
Assertion pi1xfrf 
|- ( ph -> G : B --> ( Base ` Q ) )

Proof

Step Hyp Ref Expression
1 pi1xfr.p 
 |-  P = ( J pi1 ( F ` 0 ) )
2 pi1xfr.q 
 |-  Q = ( J pi1 ( F ` 1 ) )
3 pi1xfr.b 
 |-  B = ( Base ` P )
4 pi1xfr.g 
 |-  G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
5 pi1xfr.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
6 pi1xfr.f 
 |-  ( ph -> F e. ( II Cn J ) )
7 pi1xfrval.i 
 |-  ( ph -> I e. ( II Cn J ) )
8 pi1xfrval.1 
 |-  ( ph -> ( F ` 1 ) = ( I ` 0 ) )
9 pi1xfrval.2 
 |-  ( ph -> ( I ` 1 ) = ( F ` 0 ) )
10 5 adantr 
 |-  ( ( ph /\ g e. U. B ) -> J e. ( TopOn ` X ) )
11 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
12 cnf2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` X ) /\ F e. ( II Cn J ) ) -> F : ( 0 [,] 1 ) --> X )
13 11 5 6 12 mp3an2i 
 |-  ( ph -> F : ( 0 [,] 1 ) --> X )
14 0elunit 
 |-  0 e. ( 0 [,] 1 )
15 ffvelrn 
 |-  ( ( F : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( F ` 0 ) e. X )
16 13 14 15 sylancl 
 |-  ( ph -> ( F ` 0 ) e. X )
17 16 adantr 
 |-  ( ( ph /\ g e. U. B ) -> ( F ` 0 ) e. X )
18 3 a1i 
 |-  ( ph -> B = ( Base ` P ) )
19 1 5 16 18 pi1eluni 
 |-  ( ph -> ( g e. U. B <-> ( g e. ( II Cn J ) /\ ( g ` 0 ) = ( F ` 0 ) /\ ( g ` 1 ) = ( F ` 0 ) ) ) )
20 19 biimpa 
 |-  ( ( ph /\ g e. U. B ) -> ( g e. ( II Cn J ) /\ ( g ` 0 ) = ( F ` 0 ) /\ ( g ` 1 ) = ( F ` 0 ) ) )
21 20 simp1d 
 |-  ( ( ph /\ g e. U. B ) -> g e. ( II Cn J ) )
22 20 simp2d 
 |-  ( ( ph /\ g e. U. B ) -> ( g ` 0 ) = ( F ` 0 ) )
23 20 simp3d 
 |-  ( ( ph /\ g e. U. B ) -> ( g ` 1 ) = ( F ` 0 ) )
24 1 3 10 17 21 22 23 elpi1i 
 |-  ( ( ph /\ g e. U. B ) -> [ g ] ( ~=ph ` J ) e. B )
25 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
26 1elunit 
 |-  1 e. ( 0 [,] 1 )
27 ffvelrn 
 |-  ( ( F : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( F ` 1 ) e. X )
28 13 26 27 sylancl 
 |-  ( ph -> ( F ` 1 ) e. X )
29 28 adantr 
 |-  ( ( ph /\ g e. U. B ) -> ( F ` 1 ) e. X )
30 7 adantr 
 |-  ( ( ph /\ g e. U. B ) -> I e. ( II Cn J ) )
31 6 adantr 
 |-  ( ( ph /\ g e. U. B ) -> F e. ( II Cn J ) )
32 21 31 23 pcocn 
 |-  ( ( ph /\ g e. U. B ) -> ( g ( *p ` J ) F ) e. ( II Cn J ) )
33 21 31 pco0 
 |-  ( ( ph /\ g e. U. B ) -> ( ( g ( *p ` J ) F ) ` 0 ) = ( g ` 0 ) )
34 9 adantr 
 |-  ( ( ph /\ g e. U. B ) -> ( I ` 1 ) = ( F ` 0 ) )
35 22 33 34 3eqtr4rd 
 |-  ( ( ph /\ g e. U. B ) -> ( I ` 1 ) = ( ( g ( *p ` J ) F ) ` 0 ) )
36 30 32 35 pcocn 
 |-  ( ( ph /\ g e. U. B ) -> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) e. ( II Cn J ) )
37 30 32 pco0 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 0 ) = ( I ` 0 ) )
38 8 adantr 
 |-  ( ( ph /\ g e. U. B ) -> ( F ` 1 ) = ( I ` 0 ) )
39 37 38 eqtr4d 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 0 ) = ( F ` 1 ) )
40 30 32 pco1 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 1 ) = ( ( g ( *p ` J ) F ) ` 1 ) )
41 21 31 pco1 
 |-  ( ( ph /\ g e. U. B ) -> ( ( g ( *p ` J ) F ) ` 1 ) = ( F ` 1 ) )
42 40 41 eqtrd 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 1 ) = ( F ` 1 ) )
43 2 25 10 29 36 39 42 elpi1i 
 |-  ( ( ph /\ g e. U. B ) -> [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) e. ( Base ` Q ) )
44 eceq1 
 |-  ( g = h -> [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) )
45 oveq1 
 |-  ( g = h -> ( g ( *p ` J ) F ) = ( h ( *p ` J ) F ) )
46 45 oveq2d 
 |-  ( g = h -> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) = ( I ( *p ` J ) ( h ( *p ` J ) F ) ) )
47 46 eceq1d 
 |-  ( g = h -> [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) = [ ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
48 phtpcer 
 |-  ( ~=ph ` J ) Er ( II Cn J )
49 48 a1i 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( ~=ph ` J ) Er ( II Cn J ) )
50 22 3ad2antr1 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( g ` 0 ) = ( F ` 0 ) )
51 21 3ad2antr1 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> g e. ( II Cn J ) )
52 6 adantr 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> F e. ( II Cn J ) )
53 51 52 pco0 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( ( g ( *p ` J ) F ) ` 0 ) = ( g ` 0 ) )
54 9 adantr 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( I ` 1 ) = ( F ` 0 ) )
55 50 53 54 3eqtr4rd 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( I ` 1 ) = ( ( g ( *p ` J ) F ) ` 0 ) )
56 7 adantr 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> I e. ( II Cn J ) )
57 49 56 erref 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> I ( ~=ph ` J ) I )
58 23 3ad2antr1 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( g ` 1 ) = ( F ` 0 ) )
59 simpr3 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) )
60 49 51 erth 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( g ( ~=ph ` J ) h <-> [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) )
61 59 60 mpbird 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> g ( ~=ph ` J ) h )
62 49 52 erref 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> F ( ~=ph ` J ) F )
63 58 61 62 pcohtpy 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( g ( *p ` J ) F ) ( ~=ph ` J ) ( h ( *p ` J ) F ) )
64 55 57 63 pcohtpy 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( ~=ph ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) )
65 49 64 erthi 
 |-  ( ( ph /\ ( g e. U. B /\ h e. U. B /\ [ g ] ( ~=ph ` J ) = [ h ] ( ~=ph ` J ) ) ) -> [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) = [ ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
66 4 24 43 44 47 65 fliftfund 
 |-  ( ph -> Fun G )
67 4 24 43 fliftf 
 |-  ( ph -> ( Fun G <-> G : ran ( g e. U. B |-> [ g ] ( ~=ph ` J ) ) --> ( Base ` Q ) ) )
68 66 67 mpbid 
 |-  ( ph -> G : ran ( g e. U. B |-> [ g ] ( ~=ph ` J ) ) --> ( Base ` Q ) )
69 1 5 16 18 pi1bas2 
 |-  ( ph -> B = ( U. B /. ( ~=ph ` J ) ) )
70 df-qs 
 |-  ( U. B /. ( ~=ph ` J ) ) = { s | E. g e. U. B s = [ g ] ( ~=ph ` J ) }
71 eqid 
 |-  ( g e. U. B |-> [ g ] ( ~=ph ` J ) ) = ( g e. U. B |-> [ g ] ( ~=ph ` J ) )
72 71 rnmpt 
 |-  ran ( g e. U. B |-> [ g ] ( ~=ph ` J ) ) = { s | E. g e. U. B s = [ g ] ( ~=ph ` J ) }
73 70 72 eqtr4i 
 |-  ( U. B /. ( ~=ph ` J ) ) = ran ( g e. U. B |-> [ g ] ( ~=ph ` J ) )
74 69 73 eqtrdi 
 |-  ( ph -> B = ran ( g e. U. B |-> [ g ] ( ~=ph ` J ) ) )
75 74 feq2d 
 |-  ( ph -> ( G : B --> ( Base ` Q ) <-> G : ran ( g e. U. B |-> [ g ] ( ~=ph ` J ) ) --> ( Base ` Q ) ) )
76 68 75 mpbird 
 |-  ( ph -> G : B --> ( Base ` Q ) )