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 π 1 A
pi1co.q Q = K π 1 B
pi1co.v V = Base P
pi1co.g G = ran g V g ph J F g ph K
pi1co.j φ J TopOn X
pi1co.f φ F J Cn K
pi1co.a φ A X
pi1co.b φ F A = B
Assertion pi1cof φ G : V Base Q

Proof

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