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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
ghmcnp.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
ghmcnp.k ⊢ 𝐾 = ( TopOpen ‘ 𝐻 )
Assertion ghmcnp ( ( 𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ) )

Proof

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