Metamath Proof Explorer

Theorem pi1xfrgim

Description: The mapping G between fundamental groups is an isomorphism. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses pi1xfr.p ⊢ P = J π 1 F ⁡ 0
pi1xfr.q ⊢ Q = J π 1 F ⁡ 1
pi1xfr.b ⊢ B = Base P
pi1xfr.g ⊢ G = ran ⁡ g ∈ ⋃ B ⟼ g ≃ ph ⁡ J I * 𝑝 ⁡ J g * 𝑝 ⁡ J F ≃ ph ⁡ J
pi1xfr.j ⊢ φ → J ∈ TopOn ⁡ X
pi1xfr.f ⊢ φ → F ∈ II Cn J
pi1xfr.i ⊢ I = x ∈ 0 1 ⟼ F ⁡ 1 − x
Assertion pi1xfrgim ⊢ φ → G ∈ P GrpIso Q

Proof

Step Hyp Ref Expression
1 pi1xfr.p ⊢ P = J π 1 F ⁡ 0
2 pi1xfr.q ⊢ Q = J π 1 F ⁡ 1
3 pi1xfr.b ⊢ B = Base P
4 pi1xfr.g ⊢ G = ran ⁡ g ∈ ⋃ B ⟼ g ≃ ph ⁡ J I * 𝑝 ⁡ J g * 𝑝 ⁡ J F ≃ ph ⁡ J
5 pi1xfr.j ⊢ φ → J ∈ TopOn ⁡ X
6 pi1xfr.f ⊢ φ → F ∈ II Cn J
7 pi1xfr.i ⊢ I = x ∈ 0 1 ⟼ F ⁡ 1 − x
8 1 2 3 4 5 6 7 pi1xfr ⊢ φ → G ∈ P GrpHom Q
9 eqid ⊢ ran ⁡ y ∈ ⋃ Base Q ⟼ y ≃ ph ⁡ J F * 𝑝 ⁡ J y * 𝑝 ⁡ J I ≃ ph ⁡ J = ran ⁡ y ∈ ⋃ Base Q ⟼ y ≃ ph ⁡ J F * 𝑝 ⁡ J y * 𝑝 ⁡ J I ≃ ph ⁡ J
10 1 2 3 4 5 6 7 9 pi1xfrcnv ⊢ φ → G -1 = ran ⁡ y ∈ ⋃ Base Q ⟼ y ≃ ph ⁡ J F * 𝑝 ⁡ J y * 𝑝 ⁡ J I ≃ ph ⁡ J ∧ G -1 ∈ Q GrpHom P
11 10 simprd ⊢ φ → G -1 ∈ Q GrpHom P
12 isgim2 ⊢ G ∈ P GrpIso Q ↔ G ∈ P GrpHom Q ∧ G -1 ∈ Q GrpHom P
13 8 11 12 sylanbrc ⊢ φ → G ∈ P GrpIso Q