Metamath Proof Explorer

Theorem pconnpi1

Description: All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses pconnpi1.x ⊢ 𝑋 = ∪ 𝐽
pconnpi1.p ⊢ 𝑃 = ( 𝐽 π1 𝐴 )
pconnpi1.q ⊢ 𝑄 = ( 𝐽 π1 𝐵 )
pconnpi1.s ⊢ 𝑆 = ( Base ‘ 𝑃 )
pconnpi1.t ⊢ 𝑇 = ( Base ‘ 𝑄 )
Assertion pconnpi1 ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑃 ≃𝑔 𝑄 )

Proof

Step Hyp Ref Expression
1 pconnpi1.x ⊢ 𝑋 = ∪ 𝐽
2 pconnpi1.p ⊢ 𝑃 = ( 𝐽 π1 𝐴 )
3 pconnpi1.q ⊢ 𝑄 = ( 𝐽 π1 𝐵 )
4 pconnpi1.s ⊢ 𝑆 = ( Base ‘ 𝑃 )
5 pconnpi1.t ⊢ 𝑇 = ( Base ‘ 𝑄 )
6 1 pconncn ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) )
7 eqid ⊢ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) = ( 𝐽 π1 ( 𝑓 ‘ 0 ) )
8 eqid ⊢ ( 𝐽 π1 ( 𝑓 ‘ 1 ) ) = ( 𝐽 π1 ( 𝑓 ‘ 1 ) )
9 eqid ⊢ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) = ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) )
10 eqid ⊢ ran ( ℎ ∈ ∪ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑓 ‘ ( 1 − 𝑥 ) ) ) ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝑓 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) = ran ( ℎ ∈ ∪ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑓 ‘ ( 1 − 𝑥 ) ) ) ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝑓 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
11 simpl1 ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → 𝐽 ∈ PConn )
12 pconntop ⊢ ( 𝐽 ∈ PConn → 𝐽 ∈ Top )
13 11 12 syl ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → 𝐽 ∈ Top )
14 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 13 14 sylib ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
16 simprl ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → 𝑓 ∈ ( II Cn 𝐽 ) )
17 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 1 − 𝑥 ) = ( 1 − 𝑦 ) )
18 17 fveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑓 ‘ ( 1 − 𝑥 ) ) = ( 𝑓 ‘ ( 1 − 𝑦 ) ) )
19 18 cbvmptv ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑓 ‘ ( 1 − 𝑥 ) ) ) = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑓 ‘ ( 1 − 𝑦 ) ) )
20 7 8 9 10 15 16 19 pi1xfrgim ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → ran ( ℎ ∈ ∪ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑓 ‘ ( 1 − 𝑥 ) ) ) ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝑓 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∈ ( ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) GrpIso ( 𝐽 π1 ( 𝑓 ‘ 1 ) ) ) )
21 simprrl ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → ( 𝑓 ‘ 0 ) = 𝐴 )
22 21 oveq2d ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) = ( 𝐽 π1 𝐴 ) )
23 22 2 eqtr4di ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) = 𝑃 )
24 simprrr ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → ( 𝑓 ‘ 1 ) = 𝐵 )
25 24 oveq2d ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → ( 𝐽 π1 ( 𝑓 ‘ 1 ) ) = ( 𝐽 π1 𝐵 ) )
26 25 3 eqtr4di ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → ( 𝐽 π1 ( 𝑓 ‘ 1 ) ) = 𝑄 )
27 23 26 oveq12d ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → ( ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) GrpIso ( 𝐽 π1 ( 𝑓 ‘ 1 ) ) ) = ( 𝑃 GrpIso 𝑄 ) )
28 20 27 eleqtrd ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → ran ( ℎ ∈ ∪ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑓 ‘ ( 1 − 𝑥 ) ) ) ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝑓 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∈ ( 𝑃 GrpIso 𝑄 ) )
29 brgici ⊢ ( ran ( ℎ ∈ ∪ ( Base ‘ ( 𝐽 π1 ( 𝑓 ‘ 0 ) ) ) ↦ ⟨ [ ℎ ] ( ≃ph ‘ 𝐽 ) , [ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑓 ‘ ( 1 − 𝑥 ) ) ) ( *𝑝 ‘ 𝐽 ) ( ℎ ( *𝑝 ‘ 𝐽 ) 𝑓 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∈ ( 𝑃 GrpIso 𝑄 ) → 𝑃 ≃𝑔 𝑄 )
30 28 29 syl ⊢ ( ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝐴 ∧ ( 𝑓 ‘ 1 ) = 𝐵 ) ) ) → 𝑃 ≃𝑔 𝑄 )
31 6 30 rexlimddv ⊢ ( ( 𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑃 ≃𝑔 𝑄 )