Theorem pi1coghm 22170

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 22159	. . . 4 |- ( ( J e. (TopOn ` X ) /\ A e. X ) -> P e. Grp )
5	1, 2, 4	syl2anc 673	. . 3 |- ( ph -> P e. Grp )
6		pi1co.f	. . . . . 6 |- ( ph -> F e. ( J Cn K ) )
7		cntop2 20334	. . . . . 6 |- ( F e. ( J Cn K ) -> K e. Top )
8	6, 7	syl 17	. . . . 5 |- ( ph -> K e. Top )
9		eqid 2471	. . . . . 6 |- U. K = U. K
10	9	toptopon 20025	. . . . 5 |- ( K e. Top <-> K e. (TopOn ` U. K ) )
11	8, 10	sylib 201	. . . 4 |- ( ph -> K e. (TopOn ` U. K ) )
12		pi1co.b	. . . . 5 |- ( ph -> ( F ` A ) = B )
13		cnf2 20342	. . . . . . 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 1292	. . . . . 6 |- ( ph -> F : X --> U. K )
15	14, 2	ffvelrnd 6038	. . . . 5 |- ( ph -> ( F ` A ) e. U. K )
16	12, 15	eqeltrrd 2550	. . . 4 |- ( ph -> B e. U. K )
17		pi1co.q	. . . . 5 |- Q = ( K pi1 B )
18	17	pi1grp 22159	. . . 4 |- ( ( K e. (TopOn ` U. K ) /\ B e. U. K ) -> Q e. Grp )
19	11, 16, 18	syl2anc 673	. . 3 |- ( ph -> Q e. Grp )
20	5, 19	jca 541	. 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 22168	. . 3 |- ( ph -> G : V --> ( Base ` Q ) )
24	21	a1i 11	. . . . . . . 8 |- ( ph -> V = ( Base ` P ) )
25	3, 1, 2, 24	pi1bas2 22150	. . . . . . 7 |- ( ph -> V = ( U. V /. ( ~=ph ` J ) ) )
26	25	eleq2d 2534	. . . . . 6 |- ( ph -> ( y e. V <-> y e. ( U. V /. ( ~=ph ` J ) ) ) )
27	26	biimpa 492	. . . . 5 |- ( ( ph /\ y e. V ) -> y e. ( U. V /. ( ~=ph ` J ) ) )
28		eqid 2471	. . . . . 6 |- ( U. V /. ( ~=ph ` J ) ) = ( U. V /. ( ~=ph ` J ) )
29		oveq1 6315	. . . . . . . . 9 |- ( [ f ] ( ~=ph ` J ) = y -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) = ( y ( +g ` P ) z ) )
30	29	fveq2d 5883	. . . . . . . 8 |- ( [ f ] ( ~=ph ` J ) = y -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) = ( G ` ( y ( +g ` P ) z ) ) )
31		fveq2 5879	. . . . . . . . 9 |- ( [ f ] ( ~=ph ` J ) = y -> ( G ` [ f ] ( ~=ph ` J ) ) = ( G ` y ) )
32	31	oveq1d 6323	. . . . . . . 8 |- ( [ f ] ( ~=ph ` J ) = y -> ( ( G ` [ f ] ( ~=ph ` J ) ) ( +g ` Q ) ( G ` z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
33	30, 32	eqeq12d 2486	. . . . . . 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 2829	. . . . . 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 6316	. . . . . . . . . . 11 |- ( [ h ] ( ~=ph ` J ) = z -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) = ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) )
36	35	fveq2d 5883	. . . . . . . . . 10 |- ( [ h ] ( ~=ph ` J ) = z -> ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) ) = ( G ` ( [ f ] ( ~=ph ` J ) ( +g ` P ) z ) ) )
37		fveq2 5879	. . . . . . . . . . 11 |- ( [ h ] ( ~=ph ` J ) = z -> ( G ` [ h ] ( ~=ph ` J ) ) = ( G ` z ) )
38	37	oveq2d 6324	. . . . . . . . . 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 2486	. . . . . . . . 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 22151	. . . . . . . . . . . . . . . 16 |- ( ph -> ( f e. U. V <-> ( f e. ( II Cn J ) /\ ( f ` 0 ) = A /\ ( f ` 1 ) = A ) ) )
41	40	biimpa 492	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( f e. ( II Cn J ) /\ ( f ` 0 ) = A /\ ( f ` 1 ) = A ) )
42	41	simp1d 1042	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. U. V ) -> f e. ( II Cn J ) )
43	42	adantr 472	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> f e. ( II Cn J ) )
44	1	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ f e. U. V ) -> J e. (TopOn ` X ) )
45	2	adantr 472	. . . . . . . . . . . . . . . 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 22151	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( h e. U. V <-> ( h e. ( II Cn J ) /\ ( h ` 0 ) = A /\ ( h ` 1 ) = A ) ) )
48	47	biimpa 492	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( h e. ( II Cn J ) /\ ( h ` 0 ) = A /\ ( h ` 1 ) = A ) )
49	48	simp1d 1042	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> h e. ( II Cn J ) )
50	41	simp3d 1044	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( f ` 1 ) = A )
51	50	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ` 1 ) = A )
52	48	simp2d 1043	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( h ` 0 ) = A )
53	51, 52	eqtr4d 2508	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ` 1 ) = ( h ` 0 ) )
54	6	ad2antrr 740	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> F e. ( J Cn K ) )
55	43, 49, 53, 54	copco 22127	. . . . . . . . . . . 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	55	eceq1d 7418	. . . . . . . . . . 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 ) )
57	43, 49, 53	pcocn 22126	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ( *p ` J ) h ) e. ( II Cn J ) )
58	43, 49	pco0 22123	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 0 ) = ( f ` 0 ) )
59	41	simp2d 1043	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( f ` 0 ) = A )
60	59	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ` 0 ) = A )
61	58, 60	eqtrd 2505	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 0 ) = A )
62	43, 49	pco1 22124	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 1 ) = ( h ` 1 ) )
63	48	simp3d 1044	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( h ` 1 ) = A )
64	62, 63	eqtrd 2505	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( f ( *p ` J ) h ) ` 1 ) = A )
65	1	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> J e. (TopOn ` X ) )
66	2	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> A e. X )
67	21	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> V = ( Base ` P ) )
68	3, 65, 66, 67	pi1eluni 22151	. . . . . . . . . . . . 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 ) ) )
69	57, 61, 64, 68	mpbir3and 1213	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( f ( *p ` J ) h ) e. U. V )
70	3, 17, 21, 22, 1, 6, 2, 12	pi1coval 22169	. . . . . . . . . . . . 13 |- ( ( ph /\ ( f ( *p ` J ) h ) e. U. V ) -> ( G ` [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) ) = [ ( F o. ( f ( *p ` J ) h ) ) ] ( ~=ph ` K ) )
71	70	adantlr 729	. . . . . . . . . . . 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 ) )
72	69, 71	syldan 478	. . . . . . . . . . 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 ) )
73		eqid 2471	. . . . . . . . . . . 12 |- ( Base ` Q ) = ( Base ` Q )
74	11	ad2antrr 740	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> K e. (TopOn ` U. K ) )
75	16	ad2antrr 740	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> B e. U. K )
76		eqid 2471	. . . . . . . . . . . 12 |- ( +g ` Q ) = ( +g ` Q )
77	6	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> F e. ( J Cn K ) )
78		cnco 20359	. . . . . . . . . . . . . . 15 |- ( ( f e. ( II Cn J ) /\ F e. ( J Cn K ) ) -> ( F o. f ) e. ( II Cn K ) )
79	42, 77, 78	syl2anc 673	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. U. V ) -> ( F o. f ) e. ( II Cn K ) )
80		iitopon 21989	. . . . . . . . . . . . . . . . . 18 |- II e. (TopOn ` ( 0 [,] 1 ) )
81	80	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ f e. U. V ) -> II e. (TopOn ` ( 0 [,] 1 ) ) )
82		cnf2 20342	. . . . . . . . . . . . . . . . 17 |- ( ( II e. (TopOn ` ( 0 [,] 1 ) ) /\ J e. (TopOn ` X ) /\ f e. ( II Cn J ) ) -> f : ( 0 [,] 1 ) --> X )
83	81, 44, 42, 82	syl3anc 1292	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ f e. U. V ) -> f : ( 0 [,] 1 ) --> X )
84		0elunit 11776	. . . . . . . . . . . . . . . 16 |- 0 e. ( 0 [,] 1 )
85		fvco3 5957	. . . . . . . . . . . . . . . 16 |- ( ( f : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( ( F o. f ) ` 0 ) = ( F ` ( f ` 0 ) ) )
86	83, 84, 85	sylancl 675	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 0 ) = ( F ` ( f ` 0 ) ) )
87	59	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( F ` ( f ` 0 ) ) = ( F ` A ) )
88	12	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( F ` A ) = B )
89	86, 87, 88	3eqtrd 2509	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 0 ) = B )
90		1elunit 11777	. . . . . . . . . . . . . . . 16 |- 1 e. ( 0 [,] 1 )
91		fvco3 5957	. . . . . . . . . . . . . . . 16 |- ( ( f : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. f ) ` 1 ) = ( F ` ( f ` 1 ) ) )
92	83, 90, 91	sylancl 675	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 1 ) = ( F ` ( f ` 1 ) ) )
93	50	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( F ` ( f ` 1 ) ) = ( F ` A ) )
94	92, 93, 88	3eqtrd 2509	. . . . . . . . . . . . . 14 |- ( ( ph /\ f e. U. V ) -> ( ( F o. f ) ` 1 ) = B )
95	11	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> K e. (TopOn ` U. K ) )
96	16	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> B e. U. K )
97		eqidd 2472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ f e. U. V ) -> ( Base ` Q ) = ( Base ` Q ) )
98	17, 95, 96, 97	pi1eluni 22151	. . . . . . . . . . . . . 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 ) ) )
99	79, 89, 94, 98	mpbir3and 1213	. . . . . . . . . . . . 13 |- ( ( ph /\ f e. U. V ) -> ( F o. f ) e. U. ( Base ` Q ) )
100	99	adantr 472	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. f ) e. U. ( Base ` Q ) )
101		cnco 20359	. . . . . . . . . . . . . 14 |- ( ( h e. ( II Cn J ) /\ F e. ( J Cn K ) ) -> ( F o. h ) e. ( II Cn K ) )
102	49, 54, 101	syl2anc 673	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. h ) e. ( II Cn K ) )
103	80	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> II e. (TopOn ` ( 0 [,] 1 ) ) )
104		cnf2 20342	. . . . . . . . . . . . . . . 16 |- ( ( II e. (TopOn ` ( 0 [,] 1 ) ) /\ J e. (TopOn ` X ) /\ h e. ( II Cn J ) ) -> h : ( 0 [,] 1 ) --> X )
105	103, 65, 49, 104	syl3anc 1292	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> h : ( 0 [,] 1 ) --> X )
106		fvco3 5957	. . . . . . . . . . . . . . 15 |- ( ( h : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( ( F o. h ) ` 0 ) = ( F ` ( h ` 0 ) ) )
107	105, 84, 106	sylancl 675	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 0 ) = ( F ` ( h ` 0 ) ) )
108	52	fveq2d 5883	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F ` ( h ` 0 ) ) = ( F ` A ) )
109	12	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F ` A ) = B )
110	107, 108, 109	3eqtrd 2509	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 0 ) = B )
111		fvco3 5957	. . . . . . . . . . . . . . 15 |- ( ( h : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. h ) ` 1 ) = ( F ` ( h ` 1 ) ) )
112	105, 90, 111	sylancl 675	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 1 ) = ( F ` ( h ` 1 ) ) )
113	63	fveq2d 5883	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F ` ( h ` 1 ) ) = ( F ` A ) )
114	112, 113, 109	3eqtrd 2509	. . . . . . . . . . . . 13 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( ( F o. h ) ` 1 ) = B )
115		eqidd 2472	. . . . . . . . . . . . . . 15 |- ( ph -> ( Base ` Q ) = ( Base ` Q ) )
116	17, 11, 16, 115	pi1eluni 22151	. . . . . . . . . . . . . 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 ) ) )
117	116	ad2antrr 740	. . . . . . . . . . . . 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 ) ) )
118	102, 110, 114, 117	mpbir3and 1213	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( F o. h ) e. U. ( Base ` Q ) )
119	17, 73, 74, 75, 76, 100, 118	pi1addval 22157	. . . . . . . . . . 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 ) )
120	56, 72, 119	3eqtr4d 2515	. . . . . . . . . 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 ) ) )
121		eqid 2471	. . . . . . . . . . . 12 |- ( +g ` P ) = ( +g ` P )
122		simplr 770	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> f e. U. V )
123		simpr 468	. . . . . . . . . . . 12 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> h e. U. V )
124	3, 21, 65, 66, 121, 122, 123	pi1addval 22157	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( [ f ] ( ~=ph ` J ) ( +g ` P ) [ h ] ( ~=ph ` J ) ) = [ ( f ( *p ` J ) h ) ] ( ~=ph ` J ) )
125	124	fveq2d 5883	. . . . . . . . . 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 ) ) )
126	3, 17, 21, 22, 1, 6, 2, 12	pi1coval 22169	. . . . . . . . . . . 12 |- ( ( ph /\ f e. U. V ) -> ( G ` [ f ] ( ~=ph ` J ) ) = [ ( F o. f ) ] ( ~=ph ` K ) )
127	126	adantr 472	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` [ f ] ( ~=ph ` J ) ) = [ ( F o. f ) ] ( ~=ph ` K ) )
128	3, 17, 21, 22, 1, 6, 2, 12	pi1coval 22169	. . . . . . . . . . . 12 |- ( ( ph /\ h e. U. V ) -> ( G ` [ h ] ( ~=ph ` J ) ) = [ ( F o. h ) ] ( ~=ph ` K ) )
129	128	adantlr 729	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. U. V ) /\ h e. U. V ) -> ( G ` [ h ] ( ~=ph ` J ) ) = [ ( F o. h ) ] ( ~=ph ` K ) )
130	127, 129	oveq12d 6326	. . . . . . . . . 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 ) ) )
131	120, 125, 130	3eqtr4d 2515	. . . . . . . . 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 ) ) ) )
132	28, 39, 131	ectocld 7448	. . . . . . . 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 ) ) )
133	132	ralrimiva 2809	. . . . . . 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 ) ) )
134	25	adantr 472	. . . . . . . 8 |- ( ( ph /\ f e. U. V ) -> V = ( U. V /. ( ~=ph ` J ) ) )
135	134	raleqdv 2979	. . . . . . 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 ) ) ) )
136	133, 135	mpbird 240	. . . . . 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 ) ) )
137	28, 34, 136	ectocld 7448	. . . . 5 |- ( ( ph /\ y e. ( U. V /. ( ~=ph ` J ) ) ) -> A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
138	27, 137	syldan 478	. . . 4 |- ( ( ph /\ y e. V ) -> A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
139	138	ralrimiva 2809	. . 3 |- ( ph -> A. y e. V A. z e. V ( G ` ( y ( +g ` P ) z ) ) = ( ( G ` y ) ( +g ` Q ) ( G ` z ) ) )
140	23, 139	jca 541	. 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 ) ) ) )
141	21, 73, 121, 76	isghm 16961	. 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 ) ) ) ) )
142	20, 140, 141	sylanbrc 677	1 |- ( ph -> G e. ( P GrpHom Q ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   A.wral 2756   <.cop 3965   U.cuni 4190   |-> cmpt 4454   ran crn 4840   o. ccom 4843   -->wf 5585   ` cfv 5589  (class class class)co 6308   [cec 7379   /.cqs 7380   0cc0 9557   1c1 9558   [,]cicc 11663   Basecbs 15199   +g cplusg 15268   Grpcgrp 16747   GrpHom cghm 16958   Topctop 19994  TopOnctopon 19995   Cn ccn 20317   IIcii 21985   ~=ph cphtpc 22078   *pcpco 22109   pi1 cpi1 22112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-ec 7383  df-qs 7387  df-map 7492  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-icc 11667  df-fz 11811  df-fzo 11943  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-hom 15292  df-cco 15293  df-rest 15399  df-topn 15400  df-0g 15418  df-gsum 15419  df-topgen 15420  df-pt 15421  df-prds 15424  df-xrs 15478  df-qtop 15484  df-imas 15485  df-qus 15487  df-xps 15488  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-grp 16751  df-mulg 16754  df-ghm 16959  df-cntz 17049  df-cmn 17510  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-cnfld 19048  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-cld 20111  df-cn 20320  df-cnp 20321  df-tx 20654  df-hmeo 20847  df-xms 21413  df-ms 21414  df-tms 21415  df-ii 21987  df-htpy 22079  df-phtpy 22080  df-phtpc 22101  df-pco 22114  df-om1 22115  df-pi1 22117

This theorem is referenced by: (None)