Theorem pi1coghm 20608

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
pi1coghm	|- ( ph -> G e. ( P GrpHom Q ) )

Distinct variable groups:   A, g   g, F   g, J   ph, g   g, K   P, g   Q, g   g, V

Allowed substitution hints:   B( g)   G( g)   X( g)

Proof of Theorem pi1coghm

Dummy variables h f z y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pi1co.j	. . . 4 |- ( ph -> J e. (TopOn ` X ) )
2		pi1co.a	. . . 4 |- ( ph -> A e. X )
3		pi1co.p	. . . . 5 |- P = ( J pi1 A )
4	3	pi1grp 20597	. . . 4 |- ( ( J e. (TopOn ` X ) /\ A e. X ) -> P e. Grp )
5	1, 2, 4	syl2anc 661	. . 3 |- ( ph -> P e. Grp )
6		pi1co.f	. . . . . 6 |- ( ph -> F e. ( J Cn K ) )
7		cntop2 18820	. . . . . 6 |- ( F e. ( J Cn K ) -> K e. Top )
8	6, 7	syl 16	. . . . 5 |- ( ph -> K e. Top )
9		eqid 2438	. . . . . 6 |- U. K = U. K
10	9	toptopon 18513	. . . . 5 |- ( K e. Top <-> K e. (TopOn ` U. K ) )
11	8, 10	sylib 196	. . . 4 |- ( ph -> K e. (TopOn ` U. K ) )
12		pi1co.b	. . . . 5 |- ( ph -> ( F ` A ) = B )
13		cnf2 18828	. . . . . . 7 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` U. K ) /\ F e. ( J Cn K ) ) -> F : X --> U. K )
14	1, 11, 6, 13	syl3anc 1218	. . . . . 6 |- ( ph -> F : X --> U. K )
15	14, 2	ffvelrnd 5839	. . . . 5 |- ( ph -> ( F ` A ) e. U. K )
16	12, 15	eqeltrrd 2513	. . . 4 |- ( ph -> B e. U. K )
17		pi1co.q	. . . . 5 |- Q = ( K pi1 B )
18	17	pi1grp 20597	. . . 4 |- ( ( K e. (TopOn ` U. K ) /\ B e. U. K ) -> Q e. Grp )
19	11, 16, 18	syl2anc 661	. . 3 |- ( ph -> Q e. Grp )
20	5, 19	jca 532	. 2 |- ( ph -> ( P e. Grp /\ Q e. Grp ) )
21		pi1co.v	. . . 4 |- V = ( Base ` P )
22		pi1co.g	. . . 4 |- G = ran ( g e. U. V |-> <. [ g ] ( ~=ph ` J ) , [ ( F o. g ) ] ( ~=ph ` K ) >. )
23	3, 17, 21, 22, 1, 6, 2, 12	pi1cof 20606	. . 3 |- ( ph -> G : V --> ( Base ` Q ) )
24	21	a1i 11	. . . . . . . 8 |- ( ph -> V = ( Base ` P ) )
25	3, 1, 2, 24	pi1bas2 20588	. . . . . . 7 |- ( ph -> V = ( U. V /. ( ~=ph ` J ) ) )
26	25	eleq2d 2505	. . . . . 6 |- ( ph -> ( y e. V <-> y e. ( U. V /. ( ~=ph ` J ) ) ) )
27	26	biimpa 484	. . . . 5 |- ( ( ph /\ y e. V ) -> y e. ( U. V /. ( ~=ph ` J ) ) )
28		eqid 2438	. . . . . 6 |- ( U. V /. ( ~=ph ` J ) ) = ( U. V /. ( ~=ph ` J ) )
29		oveq1 6093	. . . . . . . . 9 |- ( [ f ] ( ~=ph ` J ) = y -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) = ( y ( +g ` P ) z ) )
30	29	fveq2d 5690	. . . . . . . 8 |- ( [ f ] ( ~=ph ` J ) = y -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( G ` ( y ( +g ` P ) z ) ) )
31		fveq2 5686	. . . . . . . . 9 |- ( [ f ] ( ~=ph ` J ) = y -> ( G ` [ f ] ( ~=ph ` J ) ) = ( G ` y ) )
32	31	oveq1d 6101	. . . . . . . 8 |- ( [ f ] ( ~=ph ` J ) = y -> ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
33	30, 32	eqeq12d 2452	. . . . . . 7 |- ( [ 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 ) ) ) )
34	33	ralbidv 2730	. . . . . 6 |- ( [ 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 ) ) ) )
35		oveq2 6094	. . . . . . . . . . 11 |- ( [ h ] ( ~=ph ` J ) = z -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) = ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) )
36	35	fveq2d 5690	. . . . . . . . . 10 |- ( [ h ] ( ~=ph ` J ) = z -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) )
37		fveq2 5686	. . . . . . . . . . 11 |- ( [ h ] ( ~=ph ` J ) = z -> ( G ` [ h ] ( ~=ph ` J ) ) = ( G ` z ) )
38	37	oveq2d 6102	. . . . . . . . . 10 |- ( [ h ] ( ~=ph ` J ) = z -> ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` [ h ] ( ~=ph ` J ) ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
39	36, 38	eqeq12d 2452	. . . . . . . . 9 |- ( [ 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 ) ) ) )
40	3, 1, 2, 24	pi1eluni 20589	. . . . . . . . . . . . . . . 16 |- ( ph -> ( f e. U. V <-> ( f e. ( II Cn J ) /\ ( f ` 0 ) = A /\ ( f ` 1 ) = A ) ) )
41	40	biimpa 484	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( f e. ( II Cn J ) /\ ( f ` 0 ) = A /\ ( f ` 1 ) = A ) )
42	41	simp1d 1000	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. U. V ) -> f e. ( II Cn J ) )
43	42	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> f e. ( II Cn J ) )
44	1	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ f e. U. V ) -> J e. (TopOn ` X ) )
45	2	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ f e. U. V ) -> A e. X )
46	21	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ f e. U. V ) -> V = ( Base ` P ) )
47	3, 44, 45, 46	pi1eluni 20589	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( h e. U. V <-> ( h e. ( II Cn J ) /\ ( h ` 0 ) = A /\ ( h ` 1 ) = A ) ) )
48	47	biimpa 484	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( h e. ( II Cn J ) /\ ( h ` 0 ) = A /\ ( h ` 1 ) = A ) )
49	48	simp1d 1000	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> h e. ( II Cn J ) )
50	41	simp3d 1002	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( f ` 1 ) = A )
51	50	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ` 1 ) = A )
52	48	simp2d 1001	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( h ` 0 ) = A )
53	51, 52	eqtr4d 2473	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ` 1 ) = ( h ` 0 ) )
54	6	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> F e. ( J Cn K ) )
55	43, 49, 53, 54	copco 20565	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. ( f ( *p ` J ) h ) ) = ( ( F o. f ) ( *p ` K ) ( F o. h ) ) )
56		eceq1 7129	. . . . . . . . . . . 12 |- ( ( F o. ( f ( *p ` J ) h ) ) = ( ( F o. f ) ( *p ` K ) ( F o. h ) ) -> [ ( F o. ( f ( *p ` J ) h ) ) ] ( ~=ph ` K ) = [ ( ( F o. f ) ( *p ` K ) ( F o. h ) ) ] ( ~=ph ` K ) )
57	55, 56	syl 16	. . . . . . . . . . 11 |- ( ( ( 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 ) )
58	43, 49, 53	pcocn 20564	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ( *p ` J ) h ) e. ( II Cn J ) )
59	43, 49	pco0 20561	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 0 ) = ( f ` 0 ) )
60	41	simp2d 1001	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( f ` 0 ) = A )
61	60	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ` 0 ) = A )
62	59, 61	eqtrd 2470	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 0 ) = A )
63	43, 49	pco1 20562	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 1 ) = ( h ` 1 ) )
64	48	simp3d 1002	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( h ` 1 ) = A )
65	63, 64	eqtrd 2470	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 1 ) = A )
66	1	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> J e. (TopOn ` X ) )
67	2	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> A e. X )
68	21	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> V = ( Base ` P ) )
69	3, 66, 67, 68	pi1eluni 20589	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
70	58, 62, 65, 69	mpbir3and 1171	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ( *p ` J ) h ) e. U. V )
71	3, 17, 21, 22, 1, 6, 2, 12	pi1coval 20607	. . . . . . . . . . . . 13 |- ( ( ph /\ ( f ( *p ` J ) h ) e. U. V ) -> ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) = [ ( F o. ( f ( *p ` J ) h ) ) ] ( ~=ph ` K ) )
72	71	adantlr 714	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
73	70, 72	syldan 470	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) = [ ( F o. ( f ( *p ` J ) h ) ) ] ( ~=ph ` K ) )
74		eqid 2438	. . . . . . . . . . . 12 |- ( Base ` Q ) = ( Base ` Q )
75	11	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> K e. (TopOn ` U. K ) )
76	16	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> B e. U. K )
77		eqid 2438	. . . . . . . . . . . 12 |- ( +g ` Q ) = ( +g ` Q )
78	6	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> F e. ( J Cn K ) )
79		cnco 18845	. . . . . . . . . . . . . . 15 |- ( ( f e. ( II Cn J ) /\ F e. ( J Cn K ) ) -> ( F o. f ) e. ( II Cn K ) )
80	42, 78, 79	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. U. V ) -> ( F o. f ) e. ( II Cn K ) )
81		iitopon 20430	. . . . . . . . . . . . . . . . . 18 |- II e. (TopOn ` ( 0 [,] 1 ) )
82	81	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ f e. U. V ) -> II e. (TopOn ` ( 0 [,] 1 ) ) )
83		cnf2 18828	. . . . . . . . . . . . . . . . 17 |- ( ( II e. (TopOn ` ( 0 [,] 1 ) ) /\ J e. (TopOn ` X ) /\ f e. ( II Cn J ) ) -> f : ( 0 [,] 1 ) --> X )
84	82, 44, 42, 83	syl3anc 1218	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ f e. U. V ) -> f : ( 0 [,] 1 ) --> X )
85		0elunit 11395	. . . . . . . . . . . . . . . 16 |- 0 e. ( 0 [,] 1 )
86		fvco3 5763	. . . . . . . . . . . . . . . 16 |- ( ( f : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( ( F o. f ) ` 0 ) = ( F ` ( f ` 0 ) ) )
87	84, 85, 86	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 0 ) = ( F ` ( f ` 0 ) ) )
88	60	fveq2d 5690	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( F ` ( f ` 0 ) ) = ( F ` A ) )
89	12	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( F ` A ) = B )
90	87, 88, 89	3eqtrd 2474	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 0 ) = B )
91		1elunit 11396	. . . . . . . . . . . . . . . 16 |- 1 e. ( 0 [,] 1 )
92		fvco3 5763	. . . . . . . . . . . . . . . 16 |- ( ( f : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. f ) ` 1 ) = ( F ` ( f ` 1 ) ) )
93	84, 91, 92	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 1 ) = ( F ` ( f ` 1 ) ) )
94	50	fveq2d 5690	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( F ` ( f ` 1 ) ) = ( F ` A ) )
95	93, 94, 89	3eqtrd 2474	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 1 ) = B )
96	11	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> K e. (TopOn ` U. K ) )
97	16	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> B e. U. K )
98		eqidd 2439	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( Base ` Q ) = ( Base ` Q ) )
99	17, 96, 97, 98	pi1eluni 20589	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
100	80, 90, 95, 99	mpbir3and 1171	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. U. V ) -> ( F o. f ) e. U. ( Base ` Q ) )
101	100	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. f ) e. U. ( Base ` Q ) )
102		cnco 18845	. . . . . . . . . . . . . 14 |- ( ( h e. ( II Cn J ) /\ F e. ( J Cn K ) ) -> ( F o. h ) e. ( II Cn K ) )
103	49, 54, 102	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. h ) e. ( II Cn K ) )
104	81	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> II e. (TopOn ` ( 0 [,] 1 ) ) )
105		cnf2 18828	. . . . . . . . . . . . . . . 16 |- ( ( II e. (TopOn ` ( 0 [,] 1 ) ) /\ J e. (TopOn ` X ) /\ h e. ( II Cn J ) ) -> h : ( 0 [,] 1 ) --> X )
106	104, 66, 49, 105	syl3anc 1218	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> h : ( 0 [,] 1 ) --> X )
107		fvco3 5763	. . . . . . . . . . . . . . 15 |- ( ( h : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( ( F o. h ) ` 0 ) = ( F ` ( h ` 0 ) ) )
108	106, 85, 107	sylancl 662	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 0 ) = ( F ` ( h ` 0 ) ) )
109	52	fveq2d 5690	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F ` ( h ` 0 ) ) = ( F ` A ) )
110	12	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F ` A ) = B )
111	108, 109, 110	3eqtrd 2474	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 0 ) = B )
112		fvco3 5763	. . . . . . . . . . . . . . 15 |- ( ( h : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. h ) ` 1 ) = ( F ` ( h ` 1 ) ) )
113	106, 91, 112	sylancl 662	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 1 ) = ( F ` ( h ` 1 ) ) )
114	64	fveq2d 5690	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F ` ( h ` 1 ) ) = ( F ` A ) )
115	113, 114, 110	3eqtrd 2474	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 1 ) = B )
116		eqidd 2439	. . . . . . . . . . . . . . 15 |- ( ph -> ( Base ` Q ) = ( Base ` Q ) )
117	17, 11, 16, 116	pi1eluni 20589	. . . . . . . . . . . . . 14 |- ( 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 ) ) )
118	117	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
119	103, 111, 115, 118	mpbir3and 1171	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. h ) e. U. ( Base ` Q ) )
120	17, 74, 75, 76, 77, 101, 119	pi1addval 20595	. . . . . . . . . . 11 |- ( ( ( 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 ) )
121	57, 73, 120	3eqtr4d 2480	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
122		eqid 2438	. . . . . . . . . . . 12 |- ( +g ` P ) = ( +g ` P )
123		simplr 754	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> f e. U. V )
124		simpr 461	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> h e. U. V )
125	3, 21, 66, 67, 122, 123, 124	pi1addval 20595	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) = [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) )
126	125	fveq2d 5690	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
127	3, 17, 21, 22, 1, 6, 2, 12	pi1coval 20607	. . . . . . . . . . . 12 |- ( ( ph /\ f e. U. V ) -> ( G ` [ f ] ( ~=ph ` J ) ) = [ ( F o. f ) ] ( ~=ph ` K ) )
128	127	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` [ f ] ( ~=ph ` J ) ) = [ ( F o. f ) ] ( ~=ph ` K ) )
129	3, 17, 21, 22, 1, 6, 2, 12	pi1coval 20607	. . . . . . . . . . . 12 |- ( ( ph /\ h e. U. V ) -> ( G ` [ h ] ( ~=ph ` J ) ) = [ ( F o. h ) ] ( ~=ph ` K ) )
130	129	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` [ h ] ( ~=ph ` J ) ) = [ ( F o. h ) ] ( ~=ph ` K ) )
131	128, 130	oveq12d 6104	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
132	121, 126, 131	3eqtr4d 2480	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
133	28, 39, 132	ectocld 7159	. . . . . . . 8 |- ( ( ( 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 ) ) )
134	133	ralrimiva 2794	. . . . . . 7 |- ( ( 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 ) ) )
135	25	adantr 465	. . . . . . . 8 |- ( ( ph /\ f e. U. V ) -> V = ( U. V /. ( ~=ph ` J ) ) )
136	135	raleqdv 2918	. . . . . . 7 |- ( ( ph /\ f e. U. V ) -> ( A. z e. V ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) <-> A. z e. ( U. V /. ( ~=ph ` J ) ) ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) ) )
137	134, 136	mpbird 232	. . . . . 6 |- ( ( ph /\ f e. U. V ) -> A. z e. V ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) )
138	28, 34, 137	ectocld 7159	. . . . 5 |- ( ( ph /\ y e. ( U. V /. ( ~=ph ` J ) ) ) -> A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
139	27, 138	syldan 470	. . . 4 |- ( ( ph /\ y e. V ) -> A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
140	139	ralrimiva 2794	. . 3 |- ( ph -> A. y e. V A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
141	23, 140	jca 532	. 2 |- ( ph -> ( G : V --> ( Base ` Q ) /\ A. y e. V A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) ) )
142	21, 74, 122, 77	isghm 15738	. 2 |- ( 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 ) ) ) ) )
143	20, 141, 142	sylanbrc 664	1 |- ( ph -> G e. ( P GrpHom Q ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   A.wral 2710   <.cop 3878   U.cuni 4086   e. cmpt 4345   ran crn 4836   o. ccom 4839   -->wf 5409   ` cfv 5413  (class class class)co 6086   [cec 7091   /.cqs 7092   0cc0 9274   1c1 9275   [,]cicc 11295   Basecbs 14166   +g cplusg 14230   Grpcgrp 15402   GrpHom cghm 15735   Topctop 18473  TopOnctopon 18474   Cn ccn 18803   IIcii 20426   ~=ph cphtpc 20516   *pcpco 20547   pi1 cpi1 20550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-addf 9353  ax-mulf 9354

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-iin 4169  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-se 4675  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-recs 6824  df-rdg 6858  df-1o 6912  df-2o 6913  df-oadd 6916  df-er 7093  df-ec 7095  df-qs 7099  df-map 7208  df-ixp 7256  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-fi 7653  df-sup 7683  df-oi 7716  df-card 8101  df-cda 8329  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-q 10946  df-rp 10984  df-xneg 11081  df-xadd 11082  df-xmul 11083  df-ioo 11296  df-icc 11299  df-fz 11430  df-fzo 11541  df-seq 11799  df-exp 11858  df-hash 12096  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-struct 14168  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-mulr 14244  df-starv 14245  df-sca 14246  df-vsca 14247  df-ip 14248  df-tset 14249  df-ple 14250  df-ds 14252  df-unif 14253  df-hom 14254  df-cco 14255  df-rest 14353  df-topn 14354  df-0g 14372  df-gsum 14373  df-topgen 14374  df-pt 14375  df-prds 14378  df-xrs 14432  df-qtop 14437  df-imas 14438  df-divs 14439  df-xps 14440  df-mre 14516  df-mrc 14517  df-acs 14519  df-mnd 15407  df-submnd 15457  df-grp 15536  df-mulg 15539  df-ghm 15736  df-cntz 15826  df-cmn 16270  df-psmet 17784  df-xmet 17785  df-met 17786  df-bl 17787  df-mopn 17788  df-cnfld 17794  df-top 18478  df-bases 18480  df-topon 18481  df-topsp 18482  df-cld 18598  df-cn 18806  df-cnp 18807  df-tx 19110  df-hmeo 19303  df-xms 19870  df-ms 19871  df-tms 19872  df-ii 20428  df-htpy 20517  df-phtpy 20518  df-phtpc 20539  df-pco 20552  df-om1 20553  df-pi1 20555

This theorem is referenced by: (None)