Metamath Proof Explorer

Theorem pi1coghm

Description: The mapping G between fundamental groups is a group homomorphism. (Contributed by Mario Carneiro, 10-Aug-2015) (Revised by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses pi1co.p 
|- P = ( J pi1 A )
pi1co.q 
|- Q = ( K pi1 B )
pi1co.v 
|- V = ( Base ` P )
pi1co.g 
|- G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )
pi1co.j 
|- ( ph -> J e. ( TopOn ` X ) )
pi1co.f 
|- ( ph -> F e. ( J Cn K ) )
pi1co.a 
|- ( ph -> A e. X )
pi1co.b 
|- ( ph -> ( F ` A ) = B )
Assertion pi1coghm 
|- ( ph -> G e. ( P GrpHom Q ) )

Proof

Step Hyp Ref Expression
1 pi1co.p 
 |-  P = ( J pi1 A )
2 pi1co.q 
 |-  Q = ( K pi1 B )
3 pi1co.v 
 |-  V = ( Base ` P )
4 pi1co.g 
 |-  G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )
5 pi1co.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
6 pi1co.f 
 |-  ( ph -> F e. ( J Cn K ) )
7 pi1co.a 
 |-  ( ph -> A e. X )
8 pi1co.b 
 |-  ( ph -> ( F ` A ) = B )
9 1 pi1grp 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> P e. Grp )
10 5 7 9 syl2anc 
 |-  ( ph -> P e. Grp )
11 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
12 6 11 syl 
 |-  ( ph -> K e. Top )
13 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
14 12 13 sylib 
 |-  ( ph -> K e. ( TopOn ` U. K ) )
15 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) /\ F e. ( J Cn K ) ) -> F : X --> U. K )
16 5 14 6 15 syl3anc 
 |-  ( ph -> F : X --> U. K )
17 16 7 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. U. K )
18 8 17 eqeltrrd 
 |-  ( ph -> B e. U. K )
19 2 pi1grp 
 |-  ( ( K e. ( TopOn ` U. K ) /\ B e. U. K ) -> Q e. Grp )
20 14 18 19 syl2anc 
 |-  ( ph -> Q e. Grp )
21 1 2 3 4 5 6 7 8 pi1cof 
 |-  ( ph -> G : V --> ( Base ` Q ) )
22 3 a1i 
 |-  ( ph -> V = ( Base ` P ) )
23 1 5 7 22 pi1bas2 
 |-  ( ph -> V = ( U. V /. ( ~=ph ` J ) ) )
24 23 eleq2d 
 |-  ( ph -> ( y e. V <-> y e. ( U. V /. ( ~=ph ` J ) ) ) )
25 24 biimpa 
 |-  ( ( ph /\ y e. V ) -> y e. ( U. V /. ( ~=ph ` J ) ) )
26 eqid 
 |-  ( U. V /. ( ~=ph ` J ) ) = ( U. V /. ( ~=ph ` J ) )
27 fvoveq1 
 |-  ( [ f ] ( ~=ph ` J ) = y -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( G ` ( y ( +g ` P ) z ) ) )
28 fveq2 
 |-  ( [ f ] ( ~=ph ` J ) = y -> ( G ` [ f ] ( ~=ph ` J ) ) = ( G ` y ) )
29 28 oveq1d 
 |-  ( [ f ] ( ~=ph ` J ) = y -> ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
30 27 29 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 ) ) ) )
31 30 ralbidv 
 |-  ( [ f ] ( ~=ph ` J ) = y -> ( A. z e. V ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) <-> A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) ) )
32 oveq2 
 |-  ( [ h ] ( ~=ph ` J ) = z -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) = ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) )
33 32 fveq2d 
 |-  ( [ h ] ( ~=ph ` J ) = z -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) )
34 fveq2 
 |-  ( [ h ] ( ~=ph ` J ) = z -> ( G ` [ h ] ( ~=ph ` J ) ) = ( G ` z ) )
35 34 oveq2d 
 |-  ( [ h ] ( ~=ph ` J ) = z -> ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` [ h ] ( ~=ph ` J ) ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
36 33 35 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 ) ) ) )
37 1 5 7 22 pi1eluni 
 |-  ( ph -> ( f e. U. V <-> ( f e. ( II Cn J ) /\ ( f ` 0 ) = A /\ ( f ` 1 ) = A ) ) )
38 37 biimpa 
 |-  ( ( ph /\ f e. U. V ) -> ( f e. ( II Cn J ) /\ ( f ` 0 ) = A /\ ( f ` 1 ) = A ) )
39 38 simp1d 
 |-  ( ( ph /\ f e. U. V ) -> f e. ( II Cn J ) )
40 39 adantr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> f e. ( II Cn J ) )
41 5 adantr 
 |-  ( ( ph /\ f e. U. V ) -> J e. ( TopOn ` X ) )
42 7 adantr 
 |-  ( ( ph /\ f e. U. V ) -> A e. X )
43 3 a1i 
 |-  ( ( ph /\ f e. U. V ) -> V = ( Base ` P ) )
44 1 41 42 43 pi1eluni 
 |-  ( ( ph /\ f e. U. V ) -> ( h e. U. V <-> ( h e. ( II Cn J ) /\ ( h ` 0 ) = A /\ ( h ` 1 ) = A ) ) )
45 44 biimpa 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( h e. ( II Cn J ) /\ ( h ` 0 ) = A /\ ( h ` 1 ) = A ) )
46 45 simp1d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> h e. ( II Cn J ) )
47 38 simp3d 
 |-  ( ( ph /\ f e. U. V ) -> ( f ` 1 ) = A )
48 47 adantr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ` 1 ) = A )
49 45 simp2d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( h ` 0 ) = A )
50 48 49 eqtr4d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ` 1 ) = ( h ` 0 ) )
51 6 ad2antrr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> F e. ( J Cn K ) )
52 40 46 50 51 copco 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. ( f ( *p ` J ) h ) ) = ( ( F o. f ) ( *p ` K ) ( F o. h ) ) )
53 52 eceq1d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> [ ( F o. ( f ( *p ` J ) h ) ) ] ( ~=ph ` K ) = [ ( ( F o. f ) ( *p ` K ) ( F o. h ) ) ] ( ~=ph ` K ) )
54 40 46 50 pcocn 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ( *p ` J ) h ) e. ( II Cn J ) )
55 40 46 pco0 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 0 ) = ( f ` 0 ) )
56 38 simp2d 
 |-  ( ( ph /\ f e. U. V ) -> ( f ` 0 ) = A )
57 56 adantr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ` 0 ) = A )
58 55 57 eqtrd 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 0 ) = A )
59 40 46 pco1 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 1 ) = ( h ` 1 ) )
60 45 simp3d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( h ` 1 ) = A )
61 59 60 eqtrd 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 1 ) = A )
62 5 ad2antrr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> J e. ( TopOn ` X ) )
63 7 ad2antrr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> A e. X )
64 3 a1i 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> V = ( Base ` P ) )
65 1 62 63 64 pi1eluni 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) e. U. V <-> ( ( f ( *p ` J ) h ) e. ( II Cn J ) /\ ( ( f ( *p ` J ) h ) ` 0 ) = A /\ ( ( f ( *p ` J ) h ) ` 1 ) = A ) ) )
66 54 58 61 65 mpbir3and 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ( *p ` J ) h ) e. U. V )
67 1 2 3 4 5 6 7 8 pi1coval 
 |-  ( ( ph /\ ( f ( *p ` J ) h ) e. U. V ) -> ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) = [ ( F o. ( f ( *p ` J ) h ) ) ] ( ~=ph ` K ) )
68 67 adantlr 
 |-  ( ( ( ph /\ f e. U. V ) /\ ( f ( *p ` J ) h ) e. U. V ) -> ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) = [ ( F o. ( f ( *p ` J ) h ) ) ] ( ~=ph ` K ) )
69 66 68 syldan 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) = [ ( F o. ( f ( *p ` J ) h ) ) ] ( ~=ph ` K ) )
70 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
71 14 ad2antrr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> K e. ( TopOn ` U. K ) )
72 18 ad2antrr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> B e. U. K )
73 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
74 6 adantr 
 |-  ( ( ph /\ f e. U. V ) -> F e. ( J Cn K ) )
75 cnco 
 |-  ( ( f e. ( II Cn J ) /\ F e. ( J Cn K ) ) -> ( F o. f ) e. ( II Cn K ) )
76 39 74 75 syl2anc 
 |-  ( ( ph /\ f e. U. V ) -> ( F o. f ) e. ( II Cn K ) )
77 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
78 cnf2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` X ) /\ f e. ( II Cn J ) ) -> f : ( 0 [,] 1 ) --> X )
79 77 41 39 78 mp3an2i 
 |-  ( ( ph /\ f e. U. V ) -> f : ( 0 [,] 1 ) --> X )
80 0elunit 
 |-  0 e. ( 0 [,] 1 )
81 fvco3 
 |-  ( ( f : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( ( F o. f ) ` 0 ) = ( F ` ( f ` 0 ) ) )
82 79 80 81 sylancl 
 |-  ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 0 ) = ( F ` ( f ` 0 ) ) )
83 56 fveq2d 
 |-  ( ( ph /\ f e. U. V ) -> ( F ` ( f ` 0 ) ) = ( F ` A ) )
84 8 adantr 
 |-  ( ( ph /\ f e. U. V ) -> ( F ` A ) = B )
85 82 83 84 3eqtrd 
 |-  ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 0 ) = B )
86 1elunit 
 |-  1 e. ( 0 [,] 1 )
87 fvco3 
 |-  ( ( f : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. f ) ` 1 ) = ( F ` ( f ` 1 ) ) )
88 79 86 87 sylancl 
 |-  ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 1 ) = ( F ` ( f ` 1 ) ) )
89 47 fveq2d 
 |-  ( ( ph /\ f e. U. V ) -> ( F ` ( f ` 1 ) ) = ( F ` A ) )
90 88 89 84 3eqtrd 
 |-  ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 1 ) = B )
91 14 adantr 
 |-  ( ( ph /\ f e. U. V ) -> K e. ( TopOn ` U. K ) )
92 18 adantr 
 |-  ( ( ph /\ f e. U. V ) -> B e. U. K )
93 eqidd 
 |-  ( ( ph /\ f e. U. V ) -> ( Base ` Q ) = ( Base ` Q ) )
94 2 91 92 93 pi1eluni 
 |-  ( ( ph /\ f e. U. V ) -> ( ( F o. f ) e. U. ( Base ` Q ) <-> ( ( F o. f ) e. ( II Cn K ) /\ ( ( F o. f ) ` 0 ) = B /\ ( ( F o. f ) ` 1 ) = B ) ) )
95 76 85 90 94 mpbir3and 
 |-  ( ( ph /\ f e. U. V ) -> ( F o. f ) e. U. ( Base ` Q ) )
96 95 adantr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. f ) e. U. ( Base ` Q ) )
97 cnco 
 |-  ( ( h e. ( II Cn J ) /\ F e. ( J Cn K ) ) -> ( F o. h ) e. ( II Cn K ) )
98 46 51 97 syl2anc 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. h ) e. ( II Cn K ) )
99 cnf2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` X ) /\ h e. ( II Cn J ) ) -> h : ( 0 [,] 1 ) --> X )
100 77 62 46 99 mp3an2i 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> h : ( 0 [,] 1 ) --> X )
101 fvco3 
 |-  ( ( h : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( ( F o. h ) ` 0 ) = ( F ` ( h ` 0 ) ) )
102 100 80 101 sylancl 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 0 ) = ( F ` ( h ` 0 ) ) )
103 49 fveq2d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F ` ( h ` 0 ) ) = ( F ` A ) )
104 8 ad2antrr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F ` A ) = B )
105 102 103 104 3eqtrd 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 0 ) = B )
106 fvco3 
 |-  ( ( h : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. h ) ` 1 ) = ( F ` ( h ` 1 ) ) )
107 100 86 106 sylancl 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 1 ) = ( F ` ( h ` 1 ) ) )
108 60 fveq2d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F ` ( h ` 1 ) ) = ( F ` A ) )
109 107 108 104 3eqtrd 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 1 ) = B )
110 eqidd 
 |-  ( ph -> ( Base ` Q ) = ( Base ` Q ) )
111 2 14 18 110 pi1eluni 
 |-  ( ph -> ( ( F o. h ) e. U. ( Base ` Q ) <-> ( ( F o. h ) e. ( II Cn K ) /\ ( ( F o. h ) ` 0 ) = B /\ ( ( F o. h ) ` 1 ) = B ) ) )
112 111 ad2antrr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) e. U. ( Base ` Q ) <-> ( ( F o. h ) e. ( II Cn K ) /\ ( ( F o. h ) ` 0 ) = B /\ ( ( F o. h ) ` 1 ) = B ) ) )
113 98 105 109 112 mpbir3and 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. h ) e. U. ( Base ` Q ) )
114 2 70 71 72 73 96 113 pi1addval 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( [ ( F o. f ) ] ( ~=ph ` K ) ( +g ` Q ) [ ( F o. h ) ] ( ~=ph ` K ) ) = [ ( ( F o. f ) ( *p ` K ) ( F o. h ) ) ] ( ~=ph ` K ) )
115 53 69 114 3eqtr4d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) = ( [ ( F o. f ) ] ( ~=ph ` K ) ( +g ` Q ) [ ( F o. h ) ] ( ~=ph ` K ) ) )
116 eqid 
 |-  ( +g ` P ) = ( +g ` P )
117 simplr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> f e. U. V )
118 simpr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> h e. U. V )
119 1 3 62 63 116 117 118 pi1addval 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) = [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) )
120 119 fveq2d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) )
121 1 2 3 4 5 6 7 8 pi1coval 
 |-  ( ( ph /\ f e. U. V ) -> ( G ` [ f ] ( ~=ph ` J ) ) = [ ( F o. f ) ] ( ~=ph ` K ) )
122 121 adantr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` [ f ] ( ~=ph ` J ) ) = [ ( F o. f ) ] ( ~=ph ` K ) )
123 1 2 3 4 5 6 7 8 pi1coval 
 |-  ( ( ph /\ h e. U. V ) -> ( G ` [ h ] ( ~=ph ` J ) ) = [ ( F o. h ) ] ( ~=ph ` K ) )
124 123 adantlr 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` [ h ] ( ~=ph ` J ) ) = [ ( F o. h ) ] ( ~=ph ` K ) )
125 122 124 oveq12d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` [ h ] ( ~=ph ` J ) ) ) = ( [ ( F o. f ) ] ( ~=ph ` K ) ( +g ` Q ) [ ( F o. h ) ] ( ~=ph ` K ) ) )
126 115 120 125 3eqtr4d 
 |-  ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` [ h ] ( ~=ph ` J ) ) ) )
127 26 36 126 ectocld 
 |-  ( ( ( ph /\ f e. U. V ) /\ z e. ( U. V /. ( ~=ph ` J ) ) ) -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
128 127 ralrimiva 
 |-  ( ( ph /\ f e. U. V ) -> A. z e. ( U. V /. ( ~=ph ` J ) ) ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
129 23 adantr 
 |-  ( ( ph /\ f e. U. V ) -> V = ( U. V /. ( ~=ph ` J ) ) )
130 128 129 raleqtrrdv 
 |-  ( ( ph /\ f e. U. V ) -> A. z e. V ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
131 26 31 130 ectocld 
 |-  ( ( ph /\ y e. ( U. V /. ( ~=ph ` J ) ) ) -> A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
132 25 131 syldan 
 |-  ( ( ph /\ y e. V ) -> A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
133 132 ralrimiva 
 |-  ( ph -> A. y e. V A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
134 21 133 jca 
 |-  ( ph -> ( G : V --> ( Base ` Q ) /\ A. y e. V A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) ) )
135 3 70 116 73 isghm 
 |-  ( G e. ( P GrpHom Q ) <-> ( ( P e. Grp /\ Q e. Grp ) /\ ( G : V --> ( Base ` Q ) /\ A. y e. V A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) ) ) )
136 10 20 134 135 syl21anbrc 
 |-  ( ph -> G e. ( P GrpHom Q ) )