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π1A
pi1co.q Q=Kπ1B
pi1co.v V=BaseP
pi1co.g G=rangVgphJFgphK
pi1co.j φJTopOnX
pi1co.f φFJCnK
pi1co.a φAX
pi1co.b φFA=B
Assertion pi1cof φG:VBaseQ

Proof

Step Hyp Ref Expression
1 pi1co.p P=Jπ1A
2 pi1co.q Q=Kπ1B
3 pi1co.v V=BaseP
4 pi1co.g G=rangVgphJFgphK
5 pi1co.j φJTopOnX
6 pi1co.f φFJCnK
7 pi1co.a φAX
8 pi1co.b φFA=B
9 fvex phJV
10 ecexg phJVgphJV
11 9 10 mp1i φgVgphJV
12 eqid BaseQ=BaseQ
13 cntop2 FJCnKKTop
14 6 13 syl φKTop
15 toptopon2 KTopKTopOnK
16 14 15 sylib φKTopOnK
17 16 adantr φgVKTopOnK
18 cnf2 JTopOnXKTopOnKFJCnKF:XK
19 5 16 6 18 syl3anc φF:XK
20 19 7 ffvelrnd φFAK
21 8 20 eqeltrrd φBK
22 21 adantr φgVBK
23 3 a1i φV=BaseP
24 1 5 7 23 pi1eluni φgVgIICnJg0=Ag1=A
25 24 biimpa φgVgIICnJg0=Ag1=A
26 25 simp1d φgVgIICnJ
27 6 adantr φgVFJCnK
28 cnco gIICnJFJCnKFgIICnK
29 26 27 28 syl2anc φgVFgIICnK
30 iitopon IITopOn01
31 cnf2 IITopOn01JTopOnXgIICnJg:01X
32 30 5 26 31 mp3an2ani φgVg:01X
33 0elunit 001
34 fvco3 g:01X001Fg0=Fg0
35 32 33 34 sylancl φgVFg0=Fg0
36 25 simp2d φgVg0=A
37 36 fveq2d φgVFg0=FA
38 8 adantr φgVFA=B
39 35 37 38 3eqtrd φgVFg0=B
40 1elunit 101
41 fvco3 g:01X101Fg1=Fg1
42 32 40 41 sylancl φgVFg1=Fg1
43 25 simp3d φgVg1=A
44 43 fveq2d φgVFg1=FA
45 42 44 38 3eqtrd φgVFg1=B
46 2 12 17 22 29 39 45 elpi1i φgVFgphKBaseQ
47 eceq1 g=hgphJ=hphJ
48 coeq2 g=hFg=Fh
49 48 eceq1d g=hFgphK=FhphK
50 phtpcer phKErIICnK
51 50 a1i φgVhVgphJ=hphJphKErIICnK
52 simpr3 φgVhVgphJ=hphJgphJ=hphJ
53 phtpcer phJErIICnJ
54 53 a1i φgVhVgphJ=hphJphJErIICnJ
55 simpr1 φgVhVgphJ=hphJgV
56 24 adantr φgVhVgphJ=hphJgVgIICnJg0=Ag1=A
57 55 56 mpbid φgVhVgphJ=hphJgIICnJg0=Ag1=A
58 57 simp1d φgVhVgphJ=hphJgIICnJ
59 54 58 erth φgVhVgphJ=hphJgphJhgphJ=hphJ
60 52 59 mpbird φgVhVgphJ=hphJgphJh
61 6 adantr φgVhVgphJ=hphJFJCnK
62 60 61 phtpcco2 φgVhVgphJ=hphJFgphKFh
63 51 62 erthi φgVhVgphJ=hphJFgphK=FhphK
64 4 11 46 47 49 63 fliftfund φFunG
65 4 11 46 fliftf φFunGG:rangVgphJBaseQ
66 64 65 mpbid φG:rangVgphJBaseQ
67 1 5 7 23 pi1bas2 φV=V/phJ
68 df-qs V/phJ=s|gVs=gphJ
69 eqid gVgphJ=gVgphJ
70 69 rnmpt rangVgphJ=s|gVs=gphJ
71 68 70 eqtr4i V/phJ=rangVgphJ
72 67 71 eqtrdi φV=rangVgphJ
73 72 feq2d φG:VBaseQG:rangVgphJBaseQ
74 66 73 mpbird φG:VBaseQ