Metamath Proof Explorer

Theorem pi1xfrcnv

Description: Given a path F between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015) (Proof shortened by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses pi1xfr.p 
|- P = ( J pi1 ( F ` 0 ) )
pi1xfr.q 
|- Q = ( J pi1 ( F ` 1 ) )
pi1xfr.b 
|- B = ( Base ` P )
pi1xfr.g 
|- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
pi1xfr.j 
|- ( ph -> J e. ( TopOn ` X ) )
pi1xfr.f 
|- ( ph -> F e. ( II Cn J ) )
pi1xfr.i 
|- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
pi1xfrcnv.h 
|- H = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )
Assertion pi1xfrcnv 
|- ( ph -> ( `' G = H /\ `' G e. ( Q GrpHom P ) ) )

Proof

Step Hyp Ref Expression
1 pi1xfr.p 
 |-  P = ( J pi1 ( F ` 0 ) )
2 pi1xfr.q 
 |-  Q = ( J pi1 ( F ` 1 ) )
3 pi1xfr.b 
 |-  B = ( Base ` P )
4 pi1xfr.g 
 |-  G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
5 pi1xfr.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
6 pi1xfr.f 
 |-  ( ph -> F e. ( II Cn J ) )
7 pi1xfr.i 
 |-  I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
8 pi1xfrcnv.h 
 |-  H = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )
9 1 2 3 4 5 6 7 8 pi1xfrcnvlem 
 |-  ( ph -> `' G C_ H )
10 fvex 
 |-  ( ~=ph ` J ) e. _V
11 ecexg 
 |-  ( ( ~=ph ` J ) e. _V -> [ h ] ( ~=ph ` J ) e. _V )
12 10 11 mp1i 
 |-  ( ( ph /\ h e. U. ( Base ` Q ) ) -> [ h ] ( ~=ph ` J ) e. _V )
13 ecexg 
 |-  ( ( ~=ph ` J ) e. _V -> [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) e. _V )
14 10 13 mp1i 
 |-  ( ( ph /\ h e. U. ( Base ` Q ) ) -> [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) e. _V )
15 8 12 14 fliftrel 
 |-  ( ph -> H C_ ( _V X. _V ) )
16 df-rel 
 |-  ( Rel H <-> H C_ ( _V X. _V ) )
17 15 16 sylibr 
 |-  ( ph -> Rel H )
18 dfrel2 
 |-  ( Rel H <-> `' `' H = H )
19 17 18 sylib 
 |-  ( ph -> `' `' H = H )
20 0elunit 
 |-  0 e. ( 0 [,] 1 )
21 oveq2 
 |-  ( x = 0 -> ( 1 - x ) = ( 1 - 0 ) )
22 1m0e1 
 |-  ( 1 - 0 ) = 1
23 21 22 eqtrdi 
 |-  ( x = 0 -> ( 1 - x ) = 1 )
24 23 fveq2d 
 |-  ( x = 0 -> ( F ` ( 1 - x ) ) = ( F ` 1 ) )
25 fvex 
 |-  ( F ` 1 ) e. _V
26 24 7 25 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( I ` 0 ) = ( F ` 1 ) )
27 20 26 ax-mp 
 |-  ( I ` 0 ) = ( F ` 1 )
28 27 oveq2i 
 |-  ( J pi1 ( I ` 0 ) ) = ( J pi1 ( F ` 1 ) )
29 2 28 eqtr4i 
 |-  Q = ( J pi1 ( I ` 0 ) )
30 1elunit 
 |-  1 e. ( 0 [,] 1 )
31 oveq2 
 |-  ( x = 1 -> ( 1 - x ) = ( 1 - 1 ) )
32 31 fveq2d 
 |-  ( x = 1 -> ( F ` ( 1 - x ) ) = ( F ` ( 1 - 1 ) ) )
33 1m1e0 
 |-  ( 1 - 1 ) = 0
34 33 fveq2i 
 |-  ( F ` ( 1 - 1 ) ) = ( F ` 0 )
35 32 34 eqtrdi 
 |-  ( x = 1 -> ( F ` ( 1 - x ) ) = ( F ` 0 ) )
36 fvex 
 |-  ( F ` 0 ) e. _V
37 35 7 36 fvmpt 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( I ` 1 ) = ( F ` 0 ) )
38 30 37 ax-mp 
 |-  ( I ` 1 ) = ( F ` 0 )
39 38 oveq2i 
 |-  ( J pi1 ( I ` 1 ) ) = ( J pi1 ( F ` 0 ) )
40 1 39 eqtr4i 
 |-  P = ( J pi1 ( I ` 1 ) )
41 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
42 eqid 
 |-  ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )
43 7 pcorevcl 
 |-  ( F e. ( II Cn J ) -> ( I e. ( II Cn J ) /\ ( I ` 0 ) = ( F ` 1 ) /\ ( I ` 1 ) = ( F ` 0 ) ) )
44 6 43 syl 
 |-  ( ph -> ( I e. ( II Cn J ) /\ ( I ` 0 ) = ( F ` 1 ) /\ ( I ` 1 ) = ( F ` 0 ) ) )
45 44 simp1d 
 |-  ( ph -> I e. ( II Cn J ) )
46 oveq2 
 |-  ( z = y -> ( 1 - z ) = ( 1 - y ) )
47 46 fveq2d 
 |-  ( z = y -> ( I ` ( 1 - z ) ) = ( I ` ( 1 - y ) ) )
48 47 cbvmptv 
 |-  ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) = ( y e. ( 0 [,] 1 ) |-> ( I ` ( 1 - y ) ) )
49 eqid 
 |-  ran ( g e. U. ( Base ` P ) |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) ) ] ( ~=ph ` J ) >. ) = ran ( g e. U. ( Base ` P ) |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) ) ] ( ~=ph ` J ) >. )
50 29 40 41 42 5 45 48 49 pi1xfrcnvlem 
 |-  ( ph -> `' ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) C_ ran ( g e. U. ( Base ` P ) |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) ) ] ( ~=ph ` J ) >. ) )
51 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
52 cnf2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` X ) /\ F e. ( II Cn J ) ) -> F : ( 0 [,] 1 ) --> X )
53 51 5 6 52 mp3an2i 
 |-  ( ph -> F : ( 0 [,] 1 ) --> X )
54 53 feqmptd 
 |-  ( ph -> F = ( z e. ( 0 [,] 1 ) |-> ( F ` z ) ) )
55 iirev 
 |-  ( z e. ( 0 [,] 1 ) -> ( 1 - z ) e. ( 0 [,] 1 ) )
56 oveq2 
 |-  ( x = ( 1 - z ) -> ( 1 - x ) = ( 1 - ( 1 - z ) ) )
57 56 fveq2d 
 |-  ( x = ( 1 - z ) -> ( F ` ( 1 - x ) ) = ( F ` ( 1 - ( 1 - z ) ) ) )
58 fvex 
 |-  ( F ` ( 1 - ( 1 - z ) ) ) e. _V
59 57 7 58 fvmpt 
 |-  ( ( 1 - z ) e. ( 0 [,] 1 ) -> ( I ` ( 1 - z ) ) = ( F ` ( 1 - ( 1 - z ) ) ) )
60 55 59 syl 
 |-  ( z e. ( 0 [,] 1 ) -> ( I ` ( 1 - z ) ) = ( F ` ( 1 - ( 1 - z ) ) ) )
61 ax-1cn 
 |-  1 e. CC
62 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
63 62 sseli 
 |-  ( z e. ( 0 [,] 1 ) -> z e. RR )
64 63 recnd 
 |-  ( z e. ( 0 [,] 1 ) -> z e. CC )
65 nncan 
 |-  ( ( 1 e. CC /\ z e. CC ) -> ( 1 - ( 1 - z ) ) = z )
66 61 64 65 sylancr 
 |-  ( z e. ( 0 [,] 1 ) -> ( 1 - ( 1 - z ) ) = z )
67 66 fveq2d 
 |-  ( z e. ( 0 [,] 1 ) -> ( F ` ( 1 - ( 1 - z ) ) ) = ( F ` z ) )
68 60 67 eqtrd 
 |-  ( z e. ( 0 [,] 1 ) -> ( I ` ( 1 - z ) ) = ( F ` z ) )
69 68 mpteq2ia 
 |-  ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) = ( z e. ( 0 [,] 1 ) |-> ( F ` z ) )
70 54 69 eqtr4di 
 |-  ( ph -> F = ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) )
71 70 oveq1d 
 |-  ( ph -> ( F ( *p ` J ) ( h ( *p ` J ) I ) ) = ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) )
72 71 eceq1d 
 |-  ( ph -> [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) = [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) )
73 72 opeq2d 
 |-  ( ph -> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. = <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )
74 73 mpteq2dv 
 |-  ( ph -> ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) = ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) )
75 74 rneqd 
 |-  ( ph -> ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) )
76 8 75 eqtrid 
 |-  ( ph -> H = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) )
77 76 cnveqd 
 |-  ( ph -> `' H = `' ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) )
78 3 a1i 
 |-  ( ph -> B = ( Base ` P ) )
79 78 unieqd 
 |-  ( ph -> U. B = U. ( Base ` P ) )
80 70 oveq2d 
 |-  ( ph -> ( g ( *p ` J ) F ) = ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) )
81 80 oveq2d 
 |-  ( ph -> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) = ( I ( *p ` J ) ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) ) )
82 81 eceq1d 
 |-  ( ph -> [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) = [ ( I ( *p ` J ) ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) ) ] ( ~=ph ` J ) )
83 82 opeq2d 
 |-  ( ph -> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. = <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) ) ] ( ~=ph ` J ) >. )
84 79 83 mpteq12dv 
 |-  ( ph -> ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. ) = ( g e. U. ( Base ` P ) |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) ) ] ( ~=ph ` J ) >. ) )
85 84 rneqd 
 |-  ( ph -> ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. ) = ran ( g e. U. ( Base ` P ) |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) ) ] ( ~=ph ` J ) >. ) )
86 4 85 eqtrid 
 |-  ( ph -> G = ran ( g e. U. ( Base ` P ) |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ) ) ] ( ~=ph ` J ) >. ) )
87 50 77 86 3sstr4d 
 |-  ( ph -> `' H C_ G )
88 cnvss 
 |-  ( `' H C_ G -> `' `' H C_ `' G )
89 87 88 syl 
 |-  ( ph -> `' `' H C_ `' G )
90 19 89 eqsstrrd 
 |-  ( ph -> H C_ `' G )
91 9 90 eqssd 
 |-  ( ph -> `' G = H )
92 91 76 eqtrd 
 |-  ( ph -> `' G = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) )
93 29 40 41 42 5 45 48 pi1xfr 
 |-  ( ph -> ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( ( z e. ( 0 [,] 1 ) |-> ( I ` ( 1 - z ) ) ) ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) e. ( Q GrpHom P ) )
94 92 93 eqeltrd 
 |-  ( ph -> `' G e. ( Q GrpHom P ) )
95 91 94 jca 
 |-  ( ph -> ( `' G = H /\ `' G e. ( Q GrpHom P ) ) )