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}{\pi }_{1}{F}\left(0\right)$
pi1xfr.q ${⊢}{Q}={J}{\pi }_{1}{F}\left(1\right)$
pi1xfr.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
pi1xfr.g ${⊢}{G}=\mathrm{ran}\left({g}\in \bigcup {B}⟼⟨\left[{g}\right]{\simeq }_{\mathrm{ph}}\left({J}\right),\left[\left({I}{*}_{𝑝}\left({J}\right)\left({g}{*}_{𝑝}\left({J}\right){F}\right)\right)\right]{\simeq }_{\mathrm{ph}}\left({J}\right)⟩\right)$
pi1xfr.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
pi1xfr.f ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
pi1xfrval.i ${⊢}{\phi }\to {I}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
pi1xfrval.1 ${⊢}{\phi }\to {F}\left(1\right)={I}\left(0\right)$
pi1xfrval.2 ${⊢}{\phi }\to {I}\left(1\right)={F}\left(0\right)$
Assertion pi1xfrf ${⊢}{\phi }\to {G}:{B}⟶{\mathrm{Base}}_{{Q}}$

Proof

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