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 X = J
pconnpi1.p P = J π 1 A
pconnpi1.q Q = J π 1 B
pconnpi1.s S = Base P
pconnpi1.t T = Base Q
Assertion pconnpi1 J PConn A X B X P 𝑔 Q

Proof

Step Hyp Ref Expression
1 pconnpi1.x X = J
2 pconnpi1.p P = J π 1 A
3 pconnpi1.q Q = J π 1 B
4 pconnpi1.s S = Base P
5 pconnpi1.t T = Base Q
6 1 pconncn J PConn A X B X f II Cn J f 0 = A f 1 = B
7 eqid J π 1 f 0 = J π 1 f 0
8 eqid J π 1 f 1 = J π 1 f 1
9 eqid Base J π 1 f 0 = Base J π 1 f 0
10 eqid ran h Base J π 1 f 0 h ph J x 0 1 f 1 x * 𝑝 J h * 𝑝 J f ph J = ran h Base J π 1 f 0 h ph J x 0 1 f 1 x * 𝑝 J h * 𝑝 J f ph J
11 simpl1 J PConn A X B X f II Cn J f 0 = A f 1 = B J PConn
12 pconntop J PConn J Top
13 11 12 syl J PConn A X B X f II Cn J f 0 = A f 1 = B J Top
14 1 toptopon J Top J TopOn X
15 13 14 sylib J PConn A X B X f II Cn J f 0 = A f 1 = B J TopOn X
16 simprl J PConn A X B X f II Cn J f 0 = A f 1 = B f II Cn J
17 oveq2 x = y 1 x = 1 y
18 17 fveq2d x = y f 1 x = f 1 y
19 18 cbvmptv x 0 1 f 1 x = y 0 1 f 1 y
20 7 8 9 10 15 16 19 pi1xfrgim J PConn A X B X f II Cn J f 0 = A f 1 = B ran h Base J π 1 f 0 h ph J x 0 1 f 1 x * 𝑝 J h * 𝑝 J f ph J J π 1 f 0 GrpIso J π 1 f 1
21 simprrl J PConn A X B X f II Cn J f 0 = A f 1 = B f 0 = A
22 21 oveq2d J PConn A X B X f II Cn J f 0 = A f 1 = B J π 1 f 0 = J π 1 A
23 22 2 eqtr4di J PConn A X B X f II Cn J f 0 = A f 1 = B J π 1 f 0 = P
24 simprrr J PConn A X B X f II Cn J f 0 = A f 1 = B f 1 = B
25 24 oveq2d J PConn A X B X f II Cn J f 0 = A f 1 = B J π 1 f 1 = J π 1 B
26 25 3 eqtr4di J PConn A X B X f II Cn J f 0 = A f 1 = B J π 1 f 1 = Q
27 23 26 oveq12d J PConn A X B X f II Cn J f 0 = A f 1 = B J π 1 f 0 GrpIso J π 1 f 1 = P GrpIso Q
28 20 27 eleqtrd J PConn A X B X f II Cn J f 0 = A f 1 = B ran h Base J π 1 f 0 h ph J x 0 1 f 1 x * 𝑝 J h * 𝑝 J f ph J P GrpIso Q
29 brgici ran h Base J π 1 f 0 h ph J x 0 1 f 1 x * 𝑝 J h * 𝑝 J f ph J P GrpIso Q P 𝑔 Q
30 28 29 syl J PConn A X B X f II Cn J f 0 = A f 1 = B P 𝑔 Q
31 6 30 rexlimddv J PConn A X B X P 𝑔 Q