Metamath Proof Explorer


Theorem pi1coval

Description: The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 10-Aug-2015) (Proof shortened 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 pi1coval φTVGTphJ=FTphK

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 fvex phKV
13 ecexg phKVFgphKV
14 12 13 mp1i φgVFgphKV
15 eceq1 g=TgphJ=TphJ
16 coeq2 g=TFg=FT
17 16 eceq1d g=TFgphK=FTphK
18 1 2 3 4 5 6 7 8 pi1cof φG:VBaseQ
19 18 ffund φFunG
20 4 11 14 15 17 19 fliftval φTVGTphJ=FTphK