# 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 π 1 Y$
pi1inv.n $⊢ N = inv g ⁡ G$
pi1inv.j $⊢ φ → J ∈ TopOn ⁡ X$
pi1inv.y $⊢ φ → Y ∈ X$
pi1inv.f $⊢ φ → F ∈ II Cn J$
pi1inv.0 $⊢ φ → F ⁡ 0 = Y$
pi1inv.1 $⊢ φ → F ⁡ 1 = Y$
pi1inv.i $⊢ I = x ∈ 0 1 ⟼ F ⁡ 1 − x$
Assertion pi1inv $⊢ φ → N ⁡ F ≃ ph ⁡ J = I ≃ ph ⁡ J$

### Proof

Step Hyp Ref Expression
1 pi1grp.2 $⊢ G = J π 1 Y$
2 pi1inv.n $⊢ N = inv g ⁡ G$
3 pi1inv.j $⊢ φ → J ∈ TopOn ⁡ X$
4 pi1inv.y $⊢ φ → Y ∈ X$
5 pi1inv.f $⊢ φ → F ∈ II Cn J$
6 pi1inv.0 $⊢ φ → F ⁡ 0 = Y$
7 pi1inv.1 $⊢ φ → F ⁡ 1 = Y$
8 pi1inv.i $⊢ I = x ∈ 0 1 ⟼ F ⁡ 1 − x$
9 eqid $⊢ Base G = Base G$
10 eqid $⊢ + G = + G$
11 8 pcorevcl $⊢ F ∈ II Cn J → I ∈ II Cn J ∧ I ⁡ 0 = F ⁡ 1 ∧ I ⁡ 1 = F ⁡ 0$
12 5 11 syl $⊢ φ → I ∈ II Cn J ∧ I ⁡ 0 = F ⁡ 1 ∧ I ⁡ 1 = F ⁡ 0$
13 12 simp1d $⊢ φ → I ∈ II Cn J$
14 12 simp2d $⊢ φ → I ⁡ 0 = F ⁡ 1$
15 14 7 eqtrd $⊢ φ → I ⁡ 0 = Y$
16 12 simp3d $⊢ φ → I ⁡ 1 = F ⁡ 0$
17 16 6 eqtrd $⊢ φ → I ⁡ 1 = Y$
18 9 a1i $⊢ φ → Base G = Base G$
19 1 3 4 18 pi1eluni $⊢ φ → I ∈ ⋃ Base G ↔ I ∈ II Cn J ∧ I ⁡ 0 = Y ∧ I ⁡ 1 = Y$
20 13 15 17 19 mpbir3and $⊢ φ → I ∈ ⋃ Base G$
21 1 3 4 18 pi1eluni $⊢ φ → F ∈ ⋃ Base G ↔ F ∈ II Cn J ∧ F ⁡ 0 = Y ∧ F ⁡ 1 = Y$
22 5 6 7 21 mpbir3and $⊢ φ → F ∈ ⋃ Base G$
23 1 9 3 4 10 20 22 pi1addval $⊢ φ → I ≃ ph ⁡ J + G F ≃ ph ⁡ J = I * 𝑝 ⁡ J F ≃ ph ⁡ J$
24 phtpcer $⊢ ≃ ph ⁡ J Er II Cn J$
25 24 a1i $⊢ φ → ≃ ph ⁡ J Er II Cn J$
26 eqid $⊢ 0 1 × F ⁡ 1 = 0 1 × F ⁡ 1$
27 8 26 pcorev $⊢ F ∈ II Cn J → I * 𝑝 ⁡ J F ≃ ph ⁡ J 0 1 × F ⁡ 1$
28 5 27 syl $⊢ φ → I * 𝑝 ⁡ J F ≃ ph ⁡ J 0 1 × F ⁡ 1$
29 7 sneqd $⊢ φ → F ⁡ 1 = Y$
30 29 xpeq2d $⊢ φ → 0 1 × F ⁡ 1 = 0 1 × Y$
31 28 30 breqtrd $⊢ φ → I * 𝑝 ⁡ J F ≃ ph ⁡ J 0 1 × Y$
32 25 31 erthi $⊢ φ → I * 𝑝 ⁡ J F ≃ ph ⁡ J = 0 1 × Y ≃ ph ⁡ J$
33 eqid $⊢ 0 1 × Y = 0 1 × Y$
34 1 9 3 4 33 pi1grplem $⊢ φ → G ∈ Grp ∧ 0 1 × Y ≃ ph ⁡ J = 0 G$
35 34 simprd $⊢ φ → 0 1 × Y ≃ ph ⁡ J = 0 G$
36 23 32 35 3eqtrd $⊢ φ → I ≃ ph ⁡ J + G F ≃ ph ⁡ J = 0 G$
37 34 simpld $⊢ φ → G ∈ Grp$
38 1 9 3 4 5 6 7 elpi1i $⊢ φ → F ≃ ph ⁡ J ∈ Base G$
39 1 9 3 4 13 15 17 elpi1i $⊢ φ → I ≃ ph ⁡ J ∈ Base G$
40 eqid $⊢ 0 G = 0 G$
41 9 10 40 2 grpinvid2 $⊢ G ∈ Grp ∧ F ≃ ph ⁡ J ∈ Base G ∧ I ≃ ph ⁡ J ∈ Base G → N ⁡ F ≃ ph ⁡ J = I ≃ ph ⁡ J ↔ I ≃ ph ⁡ J + G F ≃ ph ⁡ J = 0 G$
42 37 38 39 41 syl3anc $⊢ φ → N ⁡ F ≃ ph ⁡ J = I ≃ ph ⁡ J ↔ I ≃ ph ⁡ J + G F ≃ ph ⁡ J = 0 G$
43 36 42 mpbird $⊢ φ → N ⁡ F ≃ ph ⁡ J = I ≃ ph ⁡ J$