# 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 eqtrdi $⊢ φ → 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$