Metamath Proof Explorer

Theorem pi1xfr

Description: Given a path F and its inverse I between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015)

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 ) ) )
Assertion pi1xfr 
|- ( ph -> G e. ( P GrpHom Q ) )

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 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
9 cnf2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` X ) /\ F e. ( II Cn J ) ) -> F : ( 0 [,] 1 ) --> X )
10 8 5 6 9 mp3an2i 
 |-  ( ph -> F : ( 0 [,] 1 ) --> X )
11 0elunit 
 |-  0 e. ( 0 [,] 1 )
12 ffvelrn 
 |-  ( ( F : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( F ` 0 ) e. X )
13 10 11 12 sylancl 
 |-  ( ph -> ( F ` 0 ) e. X )
14 1 pi1grp 
 |-  ( ( J e. ( TopOn ` X ) /\ ( F ` 0 ) e. X ) -> P e. Grp )
15 5 13 14 syl2anc 
 |-  ( ph -> P e. Grp )
16 1elunit 
 |-  1 e. ( 0 [,] 1 )
17 ffvelrn 
 |-  ( ( F : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( F ` 1 ) e. X )
18 10 16 17 sylancl 
 |-  ( ph -> ( F ` 1 ) e. X )
19 2 pi1grp 
 |-  ( ( J e. ( TopOn ` X ) /\ ( F ` 1 ) e. X ) -> Q e. Grp )
20 5 18 19 syl2anc 
 |-  ( ph -> Q e. Grp )
21 7 pcorevcl 
 |-  ( F e. ( II Cn J ) -> ( I e. ( II Cn J ) /\ ( I ` 0 ) = ( F ` 1 ) /\ ( I ` 1 ) = ( F ` 0 ) ) )
22 6 21 syl 
 |-  ( ph -> ( I e. ( II Cn J ) /\ ( I ` 0 ) = ( F ` 1 ) /\ ( I ` 1 ) = ( F ` 0 ) ) )
23 22 simp1d 
 |-  ( ph -> I e. ( II Cn J ) )
24 22 simp2d 
 |-  ( ph -> ( I ` 0 ) = ( F ` 1 ) )
25 24 eqcomd 
 |-  ( ph -> ( F ` 1 ) = ( I ` 0 ) )
26 22 simp3d 
 |-  ( ph -> ( I ` 1 ) = ( F ` 0 ) )
27 1 2 3 4 5 6 23 25 26 pi1xfrf 
 |-  ( ph -> G : B --> ( Base ` Q ) )
28 3 a1i 
 |-  ( ph -> B = ( Base ` P ) )
29 1 5 13 28 pi1bas2 
 |-  ( ph -> B = ( U. B /. ( ~=ph ` J ) ) )
30 29 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( U. B /. ( ~=ph ` J ) ) ) )
31 30 biimpa 
 |-  ( ( ph /\ y e. B ) -> y e. ( U. B /. ( ~=ph ` J ) ) )
32 eqid 
 |-  ( U. B /. ( ~=ph ` J ) ) = ( U. B /. ( ~=ph ` J ) )
33 fvoveq1 
 |-  ( [ f ] ( ~=ph ` J ) = y -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( G ` ( y ( +g ` P ) z ) ) )
34 fveq2 
 |-  ( [ f ] ( ~=ph ` J ) = y -> ( G ` [ f ] ( ~=ph ` J ) ) = ( G ` y ) )
35 34 oveq1d 
 |-  ( [ f ] ( ~=ph ` J ) = y -> ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
36 33 35 eqeq12d 
 |-  ( [ f ] ( ~=ph ` J ) = y -> ( ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) <-> ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) ) )
37 36 ralbidv 
 |-  ( [ f ] ( ~=ph ` J ) = y -> ( A. z e. B ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) <-> A. z e. B ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) ) )
38 29 eleq2d 
 |-  ( ph -> ( z e. B <-> z e. ( U. B /. ( ~=ph ` J ) ) ) )
39 38 biimpa 
 |-  ( ( ph /\ z e. B ) -> z e. ( U. B /. ( ~=ph ` J ) ) )
40 39 adantlr 
 |-  ( ( ( ph /\ f e. U. B ) /\ z e. B ) -> z e. ( U. B /. ( ~=ph ` J ) ) )
41 oveq2 
 |-  ( [ h ] ( ~=ph ` J ) = z -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) = ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) )
42 41 fveq2d 
 |-  ( [ h ] ( ~=ph ` J ) = z -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) )
43 fveq2 
 |-  ( [ h ] ( ~=ph ` J ) = z -> ( G ` [ h ] ( ~=ph ` J ) ) = ( G ` z ) )
44 43 oveq2d 
 |-  ( [ h ] ( ~=ph ` J ) = z -> ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` [ h ] ( ~=ph ` J ) ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
45 42 44 eqeq12d 
 |-  ( [ h ] ( ~=ph ` J ) = z -> ( ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` [ h ] ( ~=ph ` J ) ) ) <-> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) ) )
46 phtpcer 
 |-  ( ~=ph ` J ) Er ( II Cn J )
47 46 a1i 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ~=ph ` J ) Er ( II Cn J ) )
48 1 5 13 28 pi1eluni 
 |-  ( ph -> ( f e. U. B <-> ( f e. ( II Cn J ) /\ ( f ` 0 ) = ( F ` 0 ) /\ ( f ` 1 ) = ( F ` 0 ) ) ) )
49 48 biimpa 
 |-  ( ( ph /\ f e. U. B ) -> ( f e. ( II Cn J ) /\ ( f ` 0 ) = ( F ` 0 ) /\ ( f ` 1 ) = ( F ` 0 ) ) )
50 49 simp1d 
 |-  ( ( ph /\ f e. U. B ) -> f e. ( II Cn J ) )
51 50 3adant3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> f e. ( II Cn J ) )
52 1 5 13 28 pi1eluni 
 |-  ( ph -> ( h e. U. B <-> ( h e. ( II Cn J ) /\ ( h ` 0 ) = ( F ` 0 ) /\ ( h ` 1 ) = ( F ` 0 ) ) ) )
53 52 adantr 
 |-  ( ( ph /\ f e. U. B ) -> ( h e. U. B <-> ( h e. ( II Cn J ) /\ ( h ` 0 ) = ( F ` 0 ) /\ ( h ` 1 ) = ( F ` 0 ) ) ) )
54 53 biimp3a 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( h e. ( II Cn J ) /\ ( h ` 0 ) = ( F ` 0 ) /\ ( h ` 1 ) = ( F ` 0 ) ) )
55 54 simp1d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> h e. ( II Cn J ) )
56 51 55 pco0 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) h ) ` 0 ) = ( f ` 0 ) )
57 49 simp2d 
 |-  ( ( ph /\ f e. U. B ) -> ( f ` 0 ) = ( F ` 0 ) )
58 57 3adant3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( f ` 0 ) = ( F ` 0 ) )
59 56 58 eqtrd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) h ) ` 0 ) = ( F ` 0 ) )
60 49 simp3d 
 |-  ( ( ph /\ f e. U. B ) -> ( f ` 1 ) = ( F ` 0 ) )
61 60 3adant3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( f ` 1 ) = ( F ` 0 ) )
62 54 simp2d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( h ` 0 ) = ( F ` 0 ) )
63 61 62 eqtr4d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( f ` 1 ) = ( h ` 0 ) )
64 51 55 63 pcocn 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( f ( *p ` J ) h ) e. ( II Cn J ) )
65 6 3ad2ant1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> F e. ( II Cn J ) )
66 64 65 pco0 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( ( f ( *p ` J ) h ) ( *p ` J ) F ) ` 0 ) = ( ( f ( *p ` J ) h ) ` 0 ) )
67 26 3ad2ant1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ` 1 ) = ( F ` 0 ) )
68 59 66 67 3eqtr4rd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ` 1 ) = ( ( ( f ( *p ` J ) h ) ( *p ` J ) F ) ` 0 ) )
69 23 3ad2ant1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> I e. ( II Cn J ) )
70 47 69 erref 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> I ( ~=ph ` J ) I )
71 54 simp3d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( h ` 1 ) = ( F ` 0 ) )
72 eqid 
 |-  ( u e. ( 0 [,] 1 ) |-> if ( u <_ ( 1 / 2 ) , if ( u <_ ( 1 / 4 ) , ( 2 x. u ) , ( u + ( 1 / 4 ) ) ) , ( ( u / 2 ) + ( 1 / 2 ) ) ) ) = ( u e. ( 0 [,] 1 ) |-> if ( u <_ ( 1 / 2 ) , if ( u <_ ( 1 / 4 ) , ( 2 x. u ) , ( u + ( 1 / 4 ) ) ) , ( ( u / 2 ) + ( 1 / 2 ) ) ) )
73 51 55 65 63 71 72 pcoass 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) h ) ( *p ` J ) F ) ( ~=ph ` J ) ( f ( *p ` J ) ( h ( *p ` J ) F ) ) )
74 55 65 pco0 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( h ( *p ` J ) F ) ` 0 ) = ( h ` 0 ) )
75 63 74 eqtr4d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( f ` 1 ) = ( ( h ( *p ` J ) F ) ` 0 ) )
76 47 51 erref 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> f ( ~=ph ` J ) f )
77 65 69 pco1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( F ( *p ` J ) I ) ` 1 ) = ( I ` 1 ) )
78 62 74 67 3eqtr4rd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ` 1 ) = ( ( h ( *p ` J ) F ) ` 0 ) )
79 77 78 eqtrd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( F ( *p ` J ) I ) ` 1 ) = ( ( h ( *p ` J ) F ) ` 0 ) )
80 eqid 
 |-  ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } )
81 7 80 pcorev2 
 |-  ( F e. ( II Cn J ) -> ( F ( *p ` J ) I ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
82 65 81 syl 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( F ( *p ` J ) I ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
83 55 65 71 pcocn 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( h ( *p ` J ) F ) e. ( II Cn J ) )
84 47 83 erref 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( h ( *p ` J ) F ) ( ~=ph ` J ) ( h ( *p ` J ) F ) )
85 79 82 84 pcohtpy 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( F ( *p ` J ) I ) ( *p ` J ) ( h ( *p ` J ) F ) ) ( ~=ph ` J ) ( ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ( *p ` J ) ( h ( *p ` J ) F ) ) )
86 74 62 eqtrd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( h ( *p ` J ) F ) ` 0 ) = ( F ` 0 ) )
87 80 pcopt 
 |-  ( ( ( h ( *p ` J ) F ) e. ( II Cn J ) /\ ( ( h ( *p ` J ) F ) ` 0 ) = ( F ` 0 ) ) -> ( ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ( *p ` J ) ( h ( *p ` J ) F ) ) ( ~=ph ` J ) ( h ( *p ` J ) F ) )
88 83 86 87 syl2anc 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ( *p ` J ) ( h ( *p ` J ) F ) ) ( ~=ph ` J ) ( h ( *p ` J ) F ) )
89 47 85 88 ertrd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( F ( *p ` J ) I ) ( *p ` J ) ( h ( *p ` J ) F ) ) ( ~=ph ` J ) ( h ( *p ` J ) F ) )
90 24 3ad2ant1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ` 0 ) = ( F ` 1 ) )
91 90 eqcomd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( F ` 1 ) = ( I ` 0 ) )
92 65 69 83 91 78 72 pcoass 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( F ( *p ` J ) I ) ( *p ` J ) ( h ( *p ` J ) F ) ) ( ~=ph ` J ) ( F ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) )
93 47 89 92 ertr3d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( h ( *p ` J ) F ) ( ~=ph ` J ) ( F ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) )
94 75 76 93 pcohtpy 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( f ( *p ` J ) ( h ( *p ` J ) F ) ) ( ~=ph ` J ) ( f ( *p ` J ) ( F ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) ) )
95 69 83 78 pcocn 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ( *p ` J ) ( h ( *p ` J ) F ) ) e. ( II Cn J ) )
96 69 83 pco0 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ` 0 ) = ( I ` 0 ) )
97 96 90 eqtrd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ` 0 ) = ( F ` 1 ) )
98 97 eqcomd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( F ` 1 ) = ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ` 0 ) )
99 51 65 95 61 98 72 pcoass 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) F ) ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) ( ~=ph ` J ) ( f ( *p ` J ) ( F ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) ) )
100 47 94 99 ertr4d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( f ( *p ` J ) ( h ( *p ` J ) F ) ) ( ~=ph ` J ) ( ( f ( *p ` J ) F ) ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) )
101 47 73 100 ertrd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) h ) ( *p ` J ) F ) ( ~=ph ` J ) ( ( f ( *p ` J ) F ) ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) )
102 68 70 101 pcohtpy 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ( *p ` J ) ( ( f ( *p ` J ) h ) ( *p ` J ) F ) ) ( ~=ph ` J ) ( I ( *p ` J ) ( ( f ( *p ` J ) F ) ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) ) )
103 6 adantr 
 |-  ( ( ph /\ f e. U. B ) -> F e. ( II Cn J ) )
104 50 103 60 pcocn 
 |-  ( ( ph /\ f e. U. B ) -> ( f ( *p ` J ) F ) e. ( II Cn J ) )
105 104 3adant3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( f ( *p ` J ) F ) e. ( II Cn J ) )
106 50 103 pco0 
 |-  ( ( ph /\ f e. U. B ) -> ( ( f ( *p ` J ) F ) ` 0 ) = ( f ` 0 ) )
107 26 adantr 
 |-  ( ( ph /\ f e. U. B ) -> ( I ` 1 ) = ( F ` 0 ) )
108 57 106 107 3eqtr4rd 
 |-  ( ( ph /\ f e. U. B ) -> ( I ` 1 ) = ( ( f ( *p ` J ) F ) ` 0 ) )
109 108 3adant3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ` 1 ) = ( ( f ( *p ` J ) F ) ` 0 ) )
110 51 65 pco1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) F ) ` 1 ) = ( F ` 1 ) )
111 110 97 eqtr4d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) F ) ` 1 ) = ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ` 0 ) )
112 69 105 95 109 111 72 pcoass 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) ( ~=ph ` J ) ( I ( *p ` J ) ( ( f ( *p ` J ) F ) ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) ) )
113 47 102 112 ertr4d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ( *p ` J ) ( ( f ( *p ` J ) h ) ( *p ` J ) F ) ) ( ~=ph ` J ) ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) )
114 47 113 erthi 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> [ ( I ( *p ` J ) ( ( f ( *p ` J ) h ) ( *p ` J ) F ) ) ] ( ~=ph ` J ) = [ ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) ] ( ~=ph ` J ) )
115 5 3ad2ant1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> J e. ( TopOn ` X ) )
116 51 55 pco1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) h ) ` 1 ) = ( h ` 1 ) )
117 116 71 eqtrd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) h ) ` 1 ) = ( F ` 0 ) )
118 1 5 13 28 pi1eluni 
 |-  ( ph -> ( ( f ( *p ` J ) h ) e. U. B <-> ( ( f ( *p ` J ) h ) e. ( II Cn J ) /\ ( ( f ( *p ` J ) h ) ` 0 ) = ( F ` 0 ) /\ ( ( f ( *p ` J ) h ) ` 1 ) = ( F ` 0 ) ) ) )
119 118 3ad2ant1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( f ( *p ` J ) h ) e. U. B <-> ( ( f ( *p ` J ) h ) e. ( II Cn J ) /\ ( ( f ( *p ` J ) h ) ` 0 ) = ( F ` 0 ) /\ ( ( f ( *p ` J ) h ) ` 1 ) = ( F ` 0 ) ) ) )
120 64 59 117 119 mpbir3and 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( f ( *p ` J ) h ) e. U. B )
121 1 2 3 4 115 65 69 91 67 120 pi1xfrval 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) = [ ( I ( *p ` J ) ( ( f ( *p ` J ) h ) ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
122 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
123 18 3ad2ant1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( F ` 1 ) e. X )
124 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
125 23 adantr 
 |-  ( ( ph /\ f e. U. B ) -> I e. ( II Cn J ) )
126 125 104 108 pcocn 
 |-  ( ( ph /\ f e. U. B ) -> ( I ( *p ` J ) ( f ( *p ` J ) F ) ) e. ( II Cn J ) )
127 126 3adant3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ( *p ` J ) ( f ( *p ` J ) F ) ) e. ( II Cn J ) )
128 125 104 pco0 
 |-  ( ( ph /\ f e. U. B ) -> ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ` 0 ) = ( I ` 0 ) )
129 24 adantr 
 |-  ( ( ph /\ f e. U. B ) -> ( I ` 0 ) = ( F ` 1 ) )
130 128 129 eqtrd 
 |-  ( ( ph /\ f e. U. B ) -> ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ` 0 ) = ( F ` 1 ) )
131 130 3adant3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ` 0 ) = ( F ` 1 ) )
132 125 104 pco1 
 |-  ( ( ph /\ f e. U. B ) -> ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ` 1 ) = ( ( f ( *p ` J ) F ) ` 1 ) )
133 50 103 pco1 
 |-  ( ( ph /\ f e. U. B ) -> ( ( f ( *p ` J ) F ) ` 1 ) = ( F ` 1 ) )
134 132 133 eqtrd 
 |-  ( ( ph /\ f e. U. B ) -> ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ` 1 ) = ( F ` 1 ) )
135 134 3adant3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ` 1 ) = ( F ` 1 ) )
136 eqidd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( Base ` Q ) = ( Base ` Q ) )
137 2 115 123 136 pi1eluni 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) e. U. ( Base ` Q ) <-> ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) e. ( II Cn J ) /\ ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ` 0 ) = ( F ` 1 ) /\ ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ` 1 ) = ( F ` 1 ) ) ) )
138 127 131 135 137 mpbir3and 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ( *p ` J ) ( f ( *p ` J ) F ) ) e. U. ( Base ` Q ) )
139 69 83 pco1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ` 1 ) = ( ( h ( *p ` J ) F ) ` 1 ) )
140 55 65 pco1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( h ( *p ` J ) F ) ` 1 ) = ( F ` 1 ) )
141 139 140 eqtrd 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ` 1 ) = ( F ` 1 ) )
142 2 115 123 136 pi1eluni 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) e. U. ( Base ` Q ) <-> ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) e. ( II Cn J ) /\ ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ` 0 ) = ( F ` 1 ) /\ ( ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ` 1 ) = ( F ` 1 ) ) ) )
143 95 97 141 142 mpbir3and 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( I ( *p ` J ) ( h ( *p ` J ) F ) ) e. U. ( Base ` Q ) )
144 2 122 115 123 124 138 143 pi1addval 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( [ ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ] ( ~=ph ` J ) ( +g ` Q ) [ ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ] ( ~=ph ` J ) ) = [ ( ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ( *p ` J ) ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ) ] ( ~=ph ` J ) )
145 114 121 144 3eqtr4d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) = ( [ ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ] ( ~=ph ` J ) ( +g ` Q ) [ ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ] ( ~=ph ` J ) ) )
146 13 3ad2ant1 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( F ` 0 ) e. X )
147 eqid 
 |-  ( +g ` P ) = ( +g ` P )
148 simp2 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> f e. U. B )
149 simp3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> h e. U. B )
150 1 3 115 146 147 148 149 pi1addval 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) = [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) )
151 150 fveq2d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) )
152 5 adantr 
 |-  ( ( ph /\ f e. U. B ) -> J e. ( TopOn ` X ) )
153 25 adantr 
 |-  ( ( ph /\ f e. U. B ) -> ( F ` 1 ) = ( I ` 0 ) )
154 simpr 
 |-  ( ( ph /\ f e. U. B ) -> f e. U. B )
155 1 2 3 4 152 103 125 153 107 154 pi1xfrval 
 |-  ( ( ph /\ f e. U. B ) -> ( G ` [ f ] ( ~=ph ` J ) ) = [ ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
156 155 3adant3 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( G ` [ f ] ( ~=ph ` J ) ) = [ ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
157 1 2 3 4 115 65 69 91 67 149 pi1xfrval 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( G ` [ h ] ( ~=ph ` J ) ) = [ ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
158 156 157 oveq12d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` [ h ] ( ~=ph ` J ) ) ) = ( [ ( I ( *p ` J ) ( f ( *p ` J ) F ) ) ] ( ~=ph ` J ) ( +g ` Q ) [ ( I ( *p ` J ) ( h ( *p ` J ) F ) ) ] ( ~=ph ` J ) ) )
159 145 151 158 3eqtr4d 
 |-  ( ( ph /\ f e. U. B /\ h e. U. B ) -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` [ h ] ( ~=ph ` J ) ) ) )
160 159 3expa 
 |-  ( ( ( ph /\ f e. U. B ) /\ h e. U. B ) -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` [ h ] ( ~=ph ` J ) ) ) )
161 32 45 160 ectocld 
 |-  ( ( ( ph /\ f e. U. B ) /\ z e. ( U. B /. ( ~=ph ` J ) ) ) -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
162 40 161 syldan 
 |-  ( ( ( ph /\ f e. U. B ) /\ z e. B ) -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
163 162 ralrimiva 
 |-  ( ( ph /\ f e. U. B ) -> A. z e. B ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
164 32 37 163 ectocld 
 |-  ( ( ph /\ y e. ( U. B /. ( ~=ph ` J ) ) ) -> A. z e. B ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
165 31 164 syldan 
 |-  ( ( ph /\ y e. B ) -> A. z e. B ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
166 165 ralrimiva 
 |-  ( ph -> A. y e. B A. z e. B ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
167 27 166 jca 
 |-  ( ph -> ( G : B --> ( Base ` Q ) /\ A. y e. B A. z e. B ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) ) )
168 3 122 147 124 isghm 
 |-  ( G e. ( P GrpHom Q ) <-> ( ( P e. Grp /\ Q e. Grp ) /\ ( G : B --> ( Base ` Q ) /\ A. y e. B A. z e. B ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) ) ) )
169 15 20 167 168 syl21anbrc 
 |-  ( ph -> G e. ( P GrpHom Q ) )