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 = U. J
pconnpi1.p 
|- P = ( J pi1 A )
pconnpi1.q 
|- Q = ( J pi1 B )
pconnpi1.s 
|- S = ( Base ` P )
pconnpi1.t 
|- T = ( Base ` Q )
Assertion pconnpi1 
|- ( ( J e. PConn /\ A e. X /\ B e. X ) -> P ~=g Q )

Proof

Step Hyp Ref Expression
1 pconnpi1.x 
 |-  X = U. J
2 pconnpi1.p 
 |-  P = ( J pi1 A )
3 pconnpi1.q 
 |-  Q = ( J pi1 B )
4 pconnpi1.s 
 |-  S = ( Base ` P )
5 pconnpi1.t 
 |-  T = ( Base ` Q )
6 1 pconncn 
 |-  ( ( J e. PConn /\ A e. X /\ B e. X ) -> E. f e. ( II Cn J ) ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) )
7 eqid 
 |-  ( J pi1 ( f ` 0 ) ) = ( J pi1 ( f ` 0 ) )
8 eqid 
 |-  ( J pi1 ( f ` 1 ) ) = ( J pi1 ( f ` 1 ) )
9 eqid 
 |-  ( Base ` ( J pi1 ( f ` 0 ) ) ) = ( Base ` ( J pi1 ( f ` 0 ) ) )
10 eqid 
 |-  ran ( h e. U. ( Base ` ( J pi1 ( f ` 0 ) ) ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( x e. ( 0 [,] 1 ) |-> ( f ` ( 1 - x ) ) ) ( *p ` J ) ( h ( *p ` J ) f ) ) ] ( ~=ph ` J ) >. ) = ran ( h e. U. ( Base ` ( J pi1 ( f ` 0 ) ) ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( x e. ( 0 [,] 1 ) |-> ( f ` ( 1 - x ) ) ) ( *p ` J ) ( h ( *p ` J ) f ) ) ] ( ~=ph ` J ) >. )
11 simpl1 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> J e. PConn )
12 pconntop 
 |-  ( J e. PConn -> J e. Top )
13 11 12 syl 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> J e. Top )
14 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
15 13 14 sylib 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> J e. ( TopOn ` X ) )
16 simprl 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> f e. ( 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 e. ( 0 [,] 1 ) |-> ( f ` ( 1 - x ) ) ) = ( y e. ( 0 [,] 1 ) |-> ( f ` ( 1 - y ) ) )
20 7 8 9 10 15 16 19 pi1xfrgim 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> ran ( h e. U. ( Base ` ( J pi1 ( f ` 0 ) ) ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( x e. ( 0 [,] 1 ) |-> ( f ` ( 1 - x ) ) ) ( *p ` J ) ( h ( *p ` J ) f ) ) ] ( ~=ph ` J ) >. ) e. ( ( J pi1 ( f ` 0 ) ) GrpIso ( J pi1 ( f ` 1 ) ) ) )
21 simprrl 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> ( f ` 0 ) = A )
22 21 oveq2d 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> ( J pi1 ( f ` 0 ) ) = ( J pi1 A ) )
23 22 2 eqtr4di 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> ( J pi1 ( f ` 0 ) ) = P )
24 simprrr 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> ( f ` 1 ) = B )
25 24 oveq2d 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> ( J pi1 ( f ` 1 ) ) = ( J pi1 B ) )
26 25 3 eqtr4di 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> ( J pi1 ( f ` 1 ) ) = Q )
27 23 26 oveq12d 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> ( ( J pi1 ( f ` 0 ) ) GrpIso ( J pi1 ( f ` 1 ) ) ) = ( P GrpIso Q ) )
28 20 27 eleqtrd 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> ran ( h e. U. ( Base ` ( J pi1 ( f ` 0 ) ) ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( x e. ( 0 [,] 1 ) |-> ( f ` ( 1 - x ) ) ) ( *p ` J ) ( h ( *p ` J ) f ) ) ] ( ~=ph ` J ) >. ) e. ( P GrpIso Q ) )
29 brgici 
 |-  ( ran ( h e. U. ( Base ` ( J pi1 ( f ` 0 ) ) ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( x e. ( 0 [,] 1 ) |-> ( f ` ( 1 - x ) ) ) ( *p ` J ) ( h ( *p ` J ) f ) ) ] ( ~=ph ` J ) >. ) e. ( P GrpIso Q ) -> P ~=g Q )
30 28 29 syl 
 |-  ( ( ( J e. PConn /\ A e. X /\ B e. X ) /\ ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = A /\ ( f ` 1 ) = B ) ) ) -> P ~=g Q )
31 6 30 rexlimddv 
 |-  ( ( J e. PConn /\ A e. X /\ B e. X ) -> P ~=g Q )