Metamath Proof Explorer

Theorem ghmcnp

Description: A group homomorphism on topological groups is continuous everywhere if it is continuous at any point. (Contributed by Mario Carneiro, 21-Oct-2015)

Ref Expression
Hypotheses ghmcnp.x 
|- X = ( Base ` G )
ghmcnp.j 
|- J = ( TopOpen ` G )
ghmcnp.k 
|- K = ( TopOpen ` H )
Assertion ghmcnp 
|- ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( A e. X /\ F e. ( J Cn K ) ) ) )

Proof

Step Hyp Ref Expression
1 ghmcnp.x 
 |-  X = ( Base ` G )
2 ghmcnp.j 
 |-  J = ( TopOpen ` G )
3 ghmcnp.k 
 |-  K = ( TopOpen ` H )
4 eqid 
 |-  U. J = U. J
5 4 cnprcl 
 |-  ( F e. ( ( J CnP K ) ` A ) -> A e. U. J )
6 5 a1i 
 |-  ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> ( F e. ( ( J CnP K ) ` A ) -> A e. U. J ) )
7 2 1 tmdtopon 
 |-  ( G e. TopMnd -> J e. ( TopOn ` X ) )
8 7 3ad2ant1 
 |-  ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> J e. ( TopOn ` X ) )
9 8 adantr 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> J e. ( TopOn ` X ) )
10 simpl2 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> H e. TopMnd )
11 eqid 
 |-  ( Base ` H ) = ( Base ` H )
12 3 11 tmdtopon 
 |-  ( H e. TopMnd -> K e. ( TopOn ` ( Base ` H ) ) )
13 10 12 syl 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> K e. ( TopOn ` ( Base ` H ) ) )
14 simpr 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> F e. ( ( J CnP K ) ` A ) )
15 cnpf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` ( Base ` H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> F : X --> ( Base ` H ) )
16 9 13 14 15 syl3anc 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> F : X --> ( Base ` H ) )
17 16 adantr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. X ) -> F : X --> ( Base ` H ) )
18 14 adantr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> F e. ( ( J CnP K ) ` A ) )
19 eqid 
 |-  ( w e. ( Base ` H ) |-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) ) = ( w e. ( Base ` H ) |-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) )
20 19 mptpreima 
 |-  ( `' ( w e. ( Base ` H ) |-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) ) " y ) = { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y }
21 10 adantr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> H e. TopMnd )
22 16 adantr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> F : X --> ( Base ` H ) )
23 simpll3 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> F e. ( G GrpHom H ) )
24 ghmgrp1 
 |-  ( F e. ( G GrpHom H ) -> G e. Grp )
25 23 24 syl 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> G e. Grp )
26 simprl 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> x e. X )
27 5 adantl 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> A e. U. J )
28 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
29 9 28 syl 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> X = U. J )
30 27 29 eleqtrrd 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> A e. X )
31 30 adantr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> A e. X )
32 eqid 
 |-  ( -g ` G ) = ( -g ` G )
33 1 32 grpsubcl 
 |-  ( ( G e. Grp /\ x e. X /\ A e. X ) -> ( x ( -g ` G ) A ) e. X )
34 25 26 31 33 syl3anc 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( x ( -g ` G ) A ) e. X )
35 22 34 ffvelcdmd 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( F ` ( x ( -g ` G ) A ) ) e. ( Base ` H ) )
36 eqid 
 |-  ( +g ` H ) = ( +g ` H )
37 19 11 36 3 tmdlactcn 
 |-  ( ( H e. TopMnd /\ ( F ` ( x ( -g ` G ) A ) ) e. ( Base ` H ) ) -> ( w e. ( Base ` H ) |-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) ) e. ( K Cn K ) )
38 21 35 37 syl2anc 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( w e. ( Base ` H ) |-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) ) e. ( K Cn K ) )
39 simprrl 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> y e. K )
40 cnima 
 |-  ( ( ( w e. ( Base ` H ) |-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) ) e. ( K Cn K ) /\ y e. K ) -> ( `' ( w e. ( Base ` H ) |-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) ) " y ) e. K )
41 38 39 40 syl2anc 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( `' ( w e. ( Base ` H ) |-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) ) " y ) e. K )
42 20 41 eqeltrrid 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } e. K )
43 oveq2 
 |-  ( w = ( F ` A ) -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) = ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` A ) ) )
44 43 eleq1d 
 |-  ( w = ( F ` A ) -> ( ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y <-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` A ) ) e. y ) )
45 22 31 ffvelcdmd 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( F ` A ) e. ( Base ` H ) )
46 eqid 
 |-  ( -g ` H ) = ( -g ` H )
47 1 32 46 ghmsub 
 |-  ( ( F e. ( G GrpHom H ) /\ x e. X /\ A e. X ) -> ( F ` ( x ( -g ` G ) A ) ) = ( ( F ` x ) ( -g ` H ) ( F ` A ) ) )
48 23 26 31 47 syl3anc 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( F ` ( x ( -g ` G ) A ) ) = ( ( F ` x ) ( -g ` H ) ( F ` A ) ) )
49 48 oveq1d 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` A ) ) = ( ( ( F ` x ) ( -g ` H ) ( F ` A ) ) ( +g ` H ) ( F ` A ) ) )
50 ghmgrp2 
 |-  ( F e. ( G GrpHom H ) -> H e. Grp )
51 23 50 syl 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> H e. Grp )
52 22 26 ffvelcdmd 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( F ` x ) e. ( Base ` H ) )
53 11 36 46 grpnpcan 
 |-  ( ( H e. Grp /\ ( F ` x ) e. ( Base ` H ) /\ ( F ` A ) e. ( Base ` H ) ) -> ( ( ( F ` x ) ( -g ` H ) ( F ` A ) ) ( +g ` H ) ( F ` A ) ) = ( F ` x ) )
54 51 52 45 53 syl3anc 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( ( ( F ` x ) ( -g ` H ) ( F ` A ) ) ( +g ` H ) ( F ` A ) ) = ( F ` x ) )
55 49 54 eqtrd 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` A ) ) = ( F ` x ) )
56 simprrr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( F ` x ) e. y )
57 55 56 eqeltrd 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` A ) ) e. y )
58 44 45 57 elrabd 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( F ` A ) e. { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } )
59 cnpimaex 
 |-  ( ( F e. ( ( J CnP K ) ` A ) /\ { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } e. K /\ ( F ` A ) e. { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } ) -> E. z e. J ( A e. z /\ ( F " z ) C_ { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } ) )
60 18 42 58 59 syl3anc 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> E. z e. J ( A e. z /\ ( F " z ) C_ { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } ) )
61 ssrab 
 |-  ( ( F " z ) C_ { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } <-> ( ( F " z ) C_ ( Base ` H ) /\ A. w e. ( F " z ) ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y ) )
62 61 simprbi 
 |-  ( ( F " z ) C_ { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } -> A. w e. ( F " z ) ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y )
63 22 adantr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ z e. J ) -> F : X --> ( Base ` H ) )
64 63 ffnd 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ z e. J ) -> F Fn X )
65 9 adantr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> J e. ( TopOn ` X ) )
66 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. J ) -> z C_ X )
67 65 66 sylan 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ z e. J ) -> z C_ X )
68 oveq2 
 |-  ( w = ( F ` v ) -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) = ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) )
69 68 eleq1d 
 |-  ( w = ( F ` v ) -> ( ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y <-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) )
70 69 ralima 
 |-  ( ( F Fn X /\ z C_ X ) -> ( A. w e. ( F " z ) ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y <-> A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) )
71 64 67 70 syl2anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ z e. J ) -> ( A. w e. ( F " z ) ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y <-> A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) )
72 62 71 imbitrid 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ z e. J ) -> ( ( F " z ) C_ { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } -> A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) )
73 eqid 
 |-  ( w e. X |-> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) = ( w e. X |-> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) )
74 73 mptpreima 
 |-  ( `' ( w e. X |-> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) " z ) = { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z }
75 simpl1 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> G e. TopMnd )
76 75 ad2antrr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> G e. TopMnd )
77 25 adantr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> G e. Grp )
78 31 adantr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> A e. X )
79 26 adantr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> x e. X )
80 1 32 grpsubcl 
 |-  ( ( G e. Grp /\ A e. X /\ x e. X ) -> ( A ( -g ` G ) x ) e. X )
81 77 78 79 80 syl3anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> ( A ( -g ` G ) x ) e. X )
82 eqid 
 |-  ( +g ` G ) = ( +g ` G )
83 73 1 82 2 tmdlactcn 
 |-  ( ( G e. TopMnd /\ ( A ( -g ` G ) x ) e. X ) -> ( w e. X |-> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) e. ( J Cn J ) )
84 76 81 83 syl2anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> ( w e. X |-> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) e. ( J Cn J ) )
85 simprl 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> z e. J )
86 cnima 
 |-  ( ( ( w e. X |-> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) e. ( J Cn J ) /\ z e. J ) -> ( `' ( w e. X |-> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) " z ) e. J )
87 84 85 86 syl2anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> ( `' ( w e. X |-> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) " z ) e. J )
88 74 87 eqeltrrid 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } e. J )
89 oveq2 
 |-  ( w = x -> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) = ( ( A ( -g ` G ) x ) ( +g ` G ) x ) )
90 89 eleq1d 
 |-  ( w = x -> ( ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z <-> ( ( A ( -g ` G ) x ) ( +g ` G ) x ) e. z ) )
91 1 82 32 grpnpcan 
 |-  ( ( G e. Grp /\ A e. X /\ x e. X ) -> ( ( A ( -g ` G ) x ) ( +g ` G ) x ) = A )
92 77 78 79 91 syl3anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> ( ( A ( -g ` G ) x ) ( +g ` G ) x ) = A )
93 simprrl 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> A e. z )
94 92 93 eqeltrd 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> ( ( A ( -g ` G ) x ) ( +g ` G ) x ) e. z )
95 90 79 94 elrabd 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> x e. { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } )
96 simprrr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y )
97 fveq2 
 |-  ( v = ( ( A ( -g ` G ) x ) ( +g ` G ) w ) -> ( F ` v ) = ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) )
98 97 oveq2d 
 |-  ( v = ( ( A ( -g ` G ) x ) ( +g ` G ) w ) -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) = ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) )
99 98 eleq1d 
 |-  ( v = ( ( A ( -g ` G ) x ) ( +g ` G ) w ) -> ( ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y <-> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) e. y ) )
100 99 rspccv 
 |-  ( A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y -> ( ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) e. y ) )
101 96 100 syl 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> ( ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) e. y ) )
102 101 adantr 
 |-  ( ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) /\ w e. X ) -> ( ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) e. y ) )
103 23 adantr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> F e. ( G GrpHom H ) )
104 34 adantr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( x ( -g ` G ) A ) e. X )
105 103 24 syl 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> G e. Grp )
106 31 adantr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> A e. X )
107 26 adantr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> x e. X )
108 105 106 107 80 syl3anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( A ( -g ` G ) x ) e. X )
109 simpr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> w e. X )
110 1 82 grpcl 
 |-  ( ( G e. Grp /\ ( A ( -g ` G ) x ) e. X /\ w e. X ) -> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. X )
111 105 108 109 110 syl3anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. X )
112 1 82 36 ghmlin 
 |-  ( ( F e. ( G GrpHom H ) /\ ( x ( -g ` G ) A ) e. X /\ ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. X ) -> ( F ` ( ( x ( -g ` G ) A ) ( +g ` G ) ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) = ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) )
113 103 104 111 112 syl3anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( F ` ( ( x ( -g ` G ) A ) ( +g ` G ) ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) = ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) )
114 eqid 
 |-  ( invg ` G ) = ( invg ` G )
115 1 32 114 grpinvsub 
 |-  ( ( G e. Grp /\ x e. X /\ A e. X ) -> ( ( invg ` G ) ` ( x ( -g ` G ) A ) ) = ( A ( -g ` G ) x ) )
116 105 107 106 115 syl3anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( invg ` G ) ` ( x ( -g ` G ) A ) ) = ( A ( -g ` G ) x ) )
117 116 oveq2d 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) ( ( invg ` G ) ` ( x ( -g ` G ) A ) ) ) = ( ( x ( -g ` G ) A ) ( +g ` G ) ( A ( -g ` G ) x ) ) )
118 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
119 1 82 118 114 grprinv 
 |-  ( ( G e. Grp /\ ( x ( -g ` G ) A ) e. X ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) ( ( invg ` G ) ` ( x ( -g ` G ) A ) ) ) = ( 0g ` G ) )
120 105 104 119 syl2anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) ( ( invg ` G ) ` ( x ( -g ` G ) A ) ) ) = ( 0g ` G ) )
121 117 120 eqtr3d 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) ( A ( -g ` G ) x ) ) = ( 0g ` G ) )
122 121 oveq1d 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( ( x ( -g ` G ) A ) ( +g ` G ) ( A ( -g ` G ) x ) ) ( +g ` G ) w ) = ( ( 0g ` G ) ( +g ` G ) w ) )
123 1 82 grpass 
 |-  ( ( G e. Grp /\ ( ( x ( -g ` G ) A ) e. X /\ ( A ( -g ` G ) x ) e. X /\ w e. X ) ) -> ( ( ( x ( -g ` G ) A ) ( +g ` G ) ( A ( -g ` G ) x ) ) ( +g ` G ) w ) = ( ( x ( -g ` G ) A ) ( +g ` G ) ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) )
124 105 104 108 109 123 syl13anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( ( x ( -g ` G ) A ) ( +g ` G ) ( A ( -g ` G ) x ) ) ( +g ` G ) w ) = ( ( x ( -g ` G ) A ) ( +g ` G ) ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) )
125 1 82 118 grplid 
 |-  ( ( G e. Grp /\ w e. X ) -> ( ( 0g ` G ) ( +g ` G ) w ) = w )
126 105 109 125 syl2anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( 0g ` G ) ( +g ` G ) w ) = w )
127 122 124 126 3eqtr3d 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( x ( -g ` G ) A ) ( +g ` G ) ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) = w )
128 127 fveq2d 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( F ` ( ( x ( -g ` G ) A ) ( +g ` G ) ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) = ( F ` w ) )
129 113 128 eqtr3d 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ w e. X ) -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) = ( F ` w ) )
130 129 adantlr 
 |-  ( ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) /\ w e. X ) -> ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) = ( F ` w ) )
131 130 eleq1d 
 |-  ( ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) /\ w e. X ) -> ( ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` ( ( A ( -g ` G ) x ) ( +g ` G ) w ) ) ) e. y <-> ( F ` w ) e. y ) )
132 102 131 sylibd 
 |-  ( ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) /\ w e. X ) -> ( ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z -> ( F ` w ) e. y ) )
133 132 ralrimiva 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> A. w e. X ( ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z -> ( F ` w ) e. y ) )
134 fveq2 
 |-  ( v = w -> ( F ` v ) = ( F ` w ) )
135 134 eleq1d 
 |-  ( v = w -> ( ( F ` v ) e. y <-> ( F ` w ) e. y ) )
136 135 ralrab2 
 |-  ( A. v e. { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ( F ` v ) e. y <-> A. w e. X ( ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z -> ( F ` w ) e. y ) )
137 133 136 sylibr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> A. v e. { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ( F ` v ) e. y )
138 22 adantr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> F : X --> ( Base ` H ) )
139 138 ffund 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> Fun F )
140 ssrab2 
 |-  { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } C_ X
141 138 fdmd 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> dom F = X )
142 140 141 sseqtrrid 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } C_ dom F )
143 funimass4 
 |-  ( ( Fun F /\ { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } C_ dom F ) -> ( ( F " { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ) C_ y <-> A. v e. { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ( F ` v ) e. y ) )
144 139 142 143 syl2anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> ( ( F " { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ) C_ y <-> A. v e. { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ( F ` v ) e. y ) )
145 137 144 mpbird 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> ( F " { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ) C_ y )
146 eleq2 
 |-  ( u = { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } -> ( x e. u <-> x e. { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ) )
147 imaeq2 
 |-  ( u = { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } -> ( F " u ) = ( F " { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ) )
148 147 sseq1d 
 |-  ( u = { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } -> ( ( F " u ) C_ y <-> ( F " { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ) C_ y ) )
149 146 148 anbi12d 
 |-  ( u = { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } -> ( ( x e. u /\ ( F " u ) C_ y ) <-> ( x e. { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } /\ ( F " { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ) C_ y ) ) )
150 149 rspcev 
 |-  ( ( { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } e. J /\ ( x e. { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } /\ ( F " { w e. X | ( ( A ( -g ` G ) x ) ( +g ` G ) w ) e. z } ) C_ y ) ) -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) )
151 88 95 145 150 syl12anc 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ ( z e. J /\ ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) ) ) -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) )
152 151 expr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ z e. J ) -> ( ( A e. z /\ A. v e. z ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) ( F ` v ) ) e. y ) -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) ) )
153 72 152 sylan2d 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) /\ z e. J ) -> ( ( A e. z /\ ( F " z ) C_ { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } ) -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) ) )
154 153 rexlimdva 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> ( E. z e. J ( A e. z /\ ( F " z ) C_ { w e. ( Base ` H ) | ( ( F ` ( x ( -g ` G ) A ) ) ( +g ` H ) w ) e. y } ) -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) ) )
155 60 154 mpd 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( x e. X /\ ( y e. K /\ ( F ` x ) e. y ) ) ) -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) )
156 155 anassrs 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. X ) /\ ( y e. K /\ ( F ` x ) e. y ) ) -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) )
157 156 expr 
 |-  ( ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. X ) /\ y e. K ) -> ( ( F ` x ) e. y -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) ) )
158 157 ralrimiva 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. X ) -> A. y e. K ( ( F ` x ) e. y -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) ) )
159 9 adantr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. X ) -> J e. ( TopOn ` X ) )
160 13 adantr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. X ) -> K e. ( TopOn ` ( Base ` H ) ) )
161 simpr 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. X ) -> x e. X )
162 iscnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` ( Base ` H ) ) /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> ( F : X --> ( Base ` H ) /\ A. y e. K ( ( F ` x ) e. y -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) ) ) ) )
163 159 160 161 162 syl3anc 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> ( F : X --> ( Base ` H ) /\ A. y e. K ( ( F ` x ) e. y -> E. u e. J ( x e. u /\ ( F " u ) C_ y ) ) ) ) )
164 17 158 163 mpbir2and 
 |-  ( ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) /\ x e. X ) -> F e. ( ( J CnP K ) ` x ) )
165 164 ralrimiva 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> A. x e. X F e. ( ( J CnP K ) ` x ) )
166 cncnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` ( Base ` H ) ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> ( Base ` H ) /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) )
167 9 13 166 syl2anc 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> ( Base ` H ) /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) )
168 16 165 167 mpbir2and 
 |-  ( ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> F e. ( J Cn K ) )
169 168 ex 
 |-  ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> ( F e. ( ( J CnP K ) ` A ) -> F e. ( J Cn K ) ) )
170 6 169 jcad 
 |-  ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> ( F e. ( ( J CnP K ) ` A ) -> ( A e. U. J /\ F e. ( J Cn K ) ) ) )
171 4 cncnpi 
 |-  ( ( F e. ( J Cn K ) /\ A e. U. J ) -> F e. ( ( J CnP K ) ` A ) )
172 171 ancoms 
 |-  ( ( A e. U. J /\ F e. ( J Cn K ) ) -> F e. ( ( J CnP K ) ` A ) )
173 170 172 impbid1 
 |-  ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( A e. U. J /\ F e. ( J Cn K ) ) ) )
174 8 28 syl 
 |-  ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> X = U. J )
175 174 eleq2d 
 |-  ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> ( A e. X <-> A e. U. J ) )
176 175 anbi1d 
 |-  ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> ( ( A e. X /\ F e. ( J Cn K ) ) <-> ( A e. U. J /\ F e. ( J Cn K ) ) ) )
177 173 176 bitr4d 
 |-  ( ( G e. TopMnd /\ H e. TopMnd /\ F e. ( G GrpHom H ) ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( A e. X /\ F e. ( J Cn K ) ) ) )