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 π 1 F 0
pi1xfr.q Q = J π 1 F 1
pi1xfr.b B = Base P
pi1xfr.g G = ran g B g ph J I * 𝑝 J g * 𝑝 J F ph J
pi1xfr.j φ J TopOn X
pi1xfr.f φ F II Cn J
pi1xfrval.i φ I II Cn J
pi1xfrval.1 φ F 1 = I 0
pi1xfrval.2 φ I 1 = F 0
Assertion pi1xfrf φ G : B Base Q

Proof

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