# Metamath Proof Explorer

## Theorem pi1inv

Description: An inverse in the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015) (Revised by Mario Carneiro, 10-Aug-2015)

Ref Expression
Hypotheses pi1grp.2 ${⊢}{G}={J}{\pi }_{1}{Y}$
pi1inv.n ${⊢}{N}={inv}_{g}\left({G}\right)$
pi1inv.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
pi1inv.y ${⊢}{\phi }\to {Y}\in {X}$
pi1inv.f ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
pi1inv.0 ${⊢}{\phi }\to {F}\left(0\right)={Y}$
pi1inv.1 ${⊢}{\phi }\to {F}\left(1\right)={Y}$
pi1inv.i ${⊢}{I}=\left({x}\in \left[0,1\right]⟼{F}\left(1-{x}\right)\right)$
Assertion pi1inv ${⊢}{\phi }\to {N}\left(\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\right)=\left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)$

### Proof

Step Hyp Ref Expression
1 pi1grp.2 ${⊢}{G}={J}{\pi }_{1}{Y}$
2 pi1inv.n ${⊢}{N}={inv}_{g}\left({G}\right)$
3 pi1inv.j ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
4 pi1inv.y ${⊢}{\phi }\to {Y}\in {X}$
5 pi1inv.f ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
6 pi1inv.0 ${⊢}{\phi }\to {F}\left(0\right)={Y}$
7 pi1inv.1 ${⊢}{\phi }\to {F}\left(1\right)={Y}$
8 pi1inv.i ${⊢}{I}=\left({x}\in \left[0,1\right]⟼{F}\left(1-{x}\right)\right)$
9 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
10 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
11 8 pcorevcl ${⊢}{F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\to \left({I}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {I}\left(0\right)={F}\left(1\right)\wedge {I}\left(1\right)={F}\left(0\right)\right)$
12 5 11 syl ${⊢}{\phi }\to \left({I}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {I}\left(0\right)={F}\left(1\right)\wedge {I}\left(1\right)={F}\left(0\right)\right)$
13 12 simp1d ${⊢}{\phi }\to {I}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
14 12 simp2d ${⊢}{\phi }\to {I}\left(0\right)={F}\left(1\right)$
15 14 7 eqtrd ${⊢}{\phi }\to {I}\left(0\right)={Y}$
16 12 simp3d ${⊢}{\phi }\to {I}\left(1\right)={F}\left(0\right)$
17 16 6 eqtrd ${⊢}{\phi }\to {I}\left(1\right)={Y}$
18 9 a1i ${⊢}{\phi }\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
19 1 3 4 18 pi1eluni ${⊢}{\phi }\to \left({I}\in \bigcup {\mathrm{Base}}_{{G}}↔\left({I}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {I}\left(0\right)={Y}\wedge {I}\left(1\right)={Y}\right)\right)$
20 13 15 17 19 mpbir3and ${⊢}{\phi }\to {I}\in \bigcup {\mathrm{Base}}_{{G}}$
21 1 3 4 18 pi1eluni ${⊢}{\phi }\to \left({F}\in \bigcup {\mathrm{Base}}_{{G}}↔\left({F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {F}\left(0\right)={Y}\wedge {F}\left(1\right)={Y}\right)\right)$
22 5 6 7 21 mpbir3and ${⊢}{\phi }\to {F}\in \bigcup {\mathrm{Base}}_{{G}}$
23 1 9 3 4 10 20 22 pi1addval ${⊢}{\phi }\to \left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right){+}_{{G}}\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[\left({I}{*}_{𝑝}\left({J}\right){F}\right)\right]{\simeq }_{\mathrm{ph}}\left({J}\right)$
24 phtpcer ${⊢}{\simeq }_{\mathrm{ph}}\left({J}\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}{J}\right)$
25 24 a1i ${⊢}{\phi }\to {\simeq }_{\mathrm{ph}}\left({J}\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}{J}\right)$
26 eqid ${⊢}\left[0,1\right]×\left\{{F}\left(1\right)\right\}=\left[0,1\right]×\left\{{F}\left(1\right)\right\}$
27 8 26 pcorev ${⊢}{F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\to \left({I}{*}_{𝑝}\left({J}\right){F}\right){\simeq }_{\mathrm{ph}}\left({J}\right)\left(\left[0,1\right]×\left\{{F}\left(1\right)\right\}\right)$
28 5 27 syl ${⊢}{\phi }\to \left({I}{*}_{𝑝}\left({J}\right){F}\right){\simeq }_{\mathrm{ph}}\left({J}\right)\left(\left[0,1\right]×\left\{{F}\left(1\right)\right\}\right)$
29 7 sneqd ${⊢}{\phi }\to \left\{{F}\left(1\right)\right\}=\left\{{Y}\right\}$
30 29 xpeq2d ${⊢}{\phi }\to \left[0,1\right]×\left\{{F}\left(1\right)\right\}=\left[0,1\right]×\left\{{Y}\right\}$
31 28 30 breqtrd ${⊢}{\phi }\to \left({I}{*}_{𝑝}\left({J}\right){F}\right){\simeq }_{\mathrm{ph}}\left({J}\right)\left(\left[0,1\right]×\left\{{Y}\right\}\right)$
32 25 31 erthi ${⊢}{\phi }\to \left[\left({I}{*}_{𝑝}\left({J}\right){F}\right)\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[\left(\left[0,1\right]×\left\{{Y}\right\}\right)\right]{\simeq }_{\mathrm{ph}}\left({J}\right)$
33 eqid ${⊢}\left[0,1\right]×\left\{{Y}\right\}=\left[0,1\right]×\left\{{Y}\right\}$
34 1 9 3 4 33 pi1grplem ${⊢}{\phi }\to \left({G}\in \mathrm{Grp}\wedge \left[\left(\left[0,1\right]×\left\{{Y}\right\}\right)\right]{\simeq }_{\mathrm{ph}}\left({J}\right)={0}_{{G}}\right)$
35 34 simprd ${⊢}{\phi }\to \left[\left(\left[0,1\right]×\left\{{Y}\right\}\right)\right]{\simeq }_{\mathrm{ph}}\left({J}\right)={0}_{{G}}$
36 23 32 35 3eqtrd ${⊢}{\phi }\to \left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right){+}_{{G}}\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)={0}_{{G}}$
37 34 simpld ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
38 1 9 3 4 5 6 7 elpi1i ${⊢}{\phi }\to \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\in {\mathrm{Base}}_{{G}}$
39 1 9 3 4 13 15 17 elpi1i ${⊢}{\phi }\to \left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\in {\mathrm{Base}}_{{G}}$
40 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
41 9 10 40 2 grpinvid2 ${⊢}\left({G}\in \mathrm{Grp}\wedge \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\in {\mathrm{Base}}_{{G}}\wedge \left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\in {\mathrm{Base}}_{{G}}\right)\to \left({N}\left(\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\right)=\left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)↔\left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right){+}_{{G}}\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)={0}_{{G}}\right)$
42 37 38 39 41 syl3anc ${⊢}{\phi }\to \left({N}\left(\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\right)=\left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)↔\left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right){+}_{{G}}\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)={0}_{{G}}\right)$
43 36 42 mpbird ${⊢}{\phi }\to {N}\left(\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\right)=\left[{I}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)$