MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ghmcnp Structured version   Visualization version   GIF version

Theorem ghmcnp 23482
Description: A group homomorphism on topological groups is continuous everywhere if it is continuous at any point. (Contributed by Mario Carneiro, 21-Oct-2015.)
Hypotheses
Ref Expression
ghmcnp.x 𝑋 = (Baseβ€˜πΊ)
ghmcnp.j 𝐽 = (TopOpenβ€˜πΊ)
ghmcnp.k 𝐾 = (TopOpenβ€˜π»)
Assertion
Ref Expression
ghmcnp ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ (𝐴 ∈ 𝑋 ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))

Proof of Theorem ghmcnp
Dummy variables 𝑣 𝑒 𝑀 π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2733 . . . . . 6 βˆͺ 𝐽 = βˆͺ 𝐽
21cnprcl 22612 . . . . 5 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) β†’ 𝐴 ∈ βˆͺ 𝐽)
32a1i 11 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) β†’ 𝐴 ∈ βˆͺ 𝐽))
4 ghmcnp.j . . . . . . . . . 10 𝐽 = (TopOpenβ€˜πΊ)
5 ghmcnp.x . . . . . . . . . 10 𝑋 = (Baseβ€˜πΊ)
64, 5tmdtopon 23448 . . . . . . . . 9 (𝐺 ∈ TopMnd β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
763ad2ant1 1134 . . . . . . . 8 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
87adantr 482 . . . . . . 7 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
9 simpl2 1193 . . . . . . . 8 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐻 ∈ TopMnd)
10 ghmcnp.k . . . . . . . . 9 𝐾 = (TopOpenβ€˜π»)
11 eqid 2733 . . . . . . . . 9 (Baseβ€˜π») = (Baseβ€˜π»)
1210, 11tmdtopon 23448 . . . . . . . 8 (𝐻 ∈ TopMnd β†’ 𝐾 ∈ (TopOnβ€˜(Baseβ€˜π»)))
139, 12syl 17 . . . . . . 7 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐾 ∈ (TopOnβ€˜(Baseβ€˜π»)))
14 simpr 486 . . . . . . 7 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄))
15 cnpf2 22617 . . . . . . 7 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜(Baseβ€˜π»)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐹:π‘‹βŸΆ(Baseβ€˜π»))
168, 13, 14, 15syl3anc 1372 . . . . . 6 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐹:π‘‹βŸΆ(Baseβ€˜π»))
1716adantr 482 . . . . . . . 8 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ π‘₯ ∈ 𝑋) β†’ 𝐹:π‘‹βŸΆ(Baseβ€˜π»))
1814adantr 482 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄))
19 eqid 2733 . . . . . . . . . . . . . . 15 (𝑀 ∈ (Baseβ€˜π») ↦ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀)) = (𝑀 ∈ (Baseβ€˜π») ↦ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀))
2019mptpreima 6191 . . . . . . . . . . . . . 14 (β—‘(𝑀 ∈ (Baseβ€˜π») ↦ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀)) β€œ 𝑦) = {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦}
219adantr 482 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ 𝐻 ∈ TopMnd)
2216adantr 482 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ 𝐹:π‘‹βŸΆ(Baseβ€˜π»))
23 simpll3 1215 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ 𝐹 ∈ (𝐺 GrpHom 𝐻))
24 ghmgrp1 19015 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (𝐺 GrpHom 𝐻) β†’ 𝐺 ∈ Grp)
2523, 24syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ 𝐺 ∈ Grp)
26 simprl 770 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ π‘₯ ∈ 𝑋)
272adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐴 ∈ βˆͺ 𝐽)
28 toponuni 22279 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
298, 28syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝑋 = βˆͺ 𝐽)
3027, 29eleqtrrd 2837 . . . . . . . . . . . . . . . . . . 19 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐴 ∈ 𝑋)
3130adantr 482 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ 𝐴 ∈ 𝑋)
32 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (-gβ€˜πΊ) = (-gβ€˜πΊ)
335, 32grpsubcl 18832 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ π‘₯ ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) β†’ (π‘₯(-gβ€˜πΊ)𝐴) ∈ 𝑋)
3425, 26, 31, 33syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (π‘₯(-gβ€˜πΊ)𝐴) ∈ 𝑋)
3522, 34ffvelcdmd 7037 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴)) ∈ (Baseβ€˜π»))
36 eqid 2733 . . . . . . . . . . . . . . . . 17 (+gβ€˜π») = (+gβ€˜π»)
3719, 11, 36, 10tmdlactcn 23469 . . . . . . . . . . . . . . . 16 ((𝐻 ∈ TopMnd ∧ (πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴)) ∈ (Baseβ€˜π»)) β†’ (𝑀 ∈ (Baseβ€˜π») ↦ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀)) ∈ (𝐾 Cn 𝐾))
3821, 35, 37syl2anc 585 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (𝑀 ∈ (Baseβ€˜π») ↦ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀)) ∈ (𝐾 Cn 𝐾))
39 simprrl 780 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ 𝑦 ∈ 𝐾)
40 cnima 22632 . . . . . . . . . . . . . . 15 (((𝑀 ∈ (Baseβ€˜π») ↦ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀)) ∈ (𝐾 Cn 𝐾) ∧ 𝑦 ∈ 𝐾) β†’ (β—‘(𝑀 ∈ (Baseβ€˜π») ↦ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀)) β€œ 𝑦) ∈ 𝐾)
4138, 39, 40syl2anc 585 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (β—‘(𝑀 ∈ (Baseβ€˜π») ↦ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀)) β€œ 𝑦) ∈ 𝐾)
4220, 41eqeltrrid 2839 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦} ∈ 𝐾)
43 oveq2 7366 . . . . . . . . . . . . . . 15 (𝑀 = (πΉβ€˜π΄) β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) = ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π΄)))
4443eleq1d 2819 . . . . . . . . . . . . . 14 (𝑀 = (πΉβ€˜π΄) β†’ (((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦 ↔ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π΄)) ∈ 𝑦))
4522, 31ffvelcdmd 7037 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (πΉβ€˜π΄) ∈ (Baseβ€˜π»))
46 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (-gβ€˜π») = (-gβ€˜π»)
475, 32, 46ghmsub 19021 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ π‘₯ ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) β†’ (πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴)) = ((πΉβ€˜π‘₯)(-gβ€˜π»)(πΉβ€˜π΄)))
4823, 26, 31, 47syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴)) = ((πΉβ€˜π‘₯)(-gβ€˜π»)(πΉβ€˜π΄)))
4948oveq1d 7373 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π΄)) = (((πΉβ€˜π‘₯)(-gβ€˜π»)(πΉβ€˜π΄))(+gβ€˜π»)(πΉβ€˜π΄)))
50 ghmgrp2 19016 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (𝐺 GrpHom 𝐻) β†’ 𝐻 ∈ Grp)
5123, 50syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ 𝐻 ∈ Grp)
5222, 26ffvelcdmd 7037 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (πΉβ€˜π‘₯) ∈ (Baseβ€˜π»))
5311, 36, 46grpnpcan 18844 . . . . . . . . . . . . . . . . 17 ((𝐻 ∈ Grp ∧ (πΉβ€˜π‘₯) ∈ (Baseβ€˜π») ∧ (πΉβ€˜π΄) ∈ (Baseβ€˜π»)) β†’ (((πΉβ€˜π‘₯)(-gβ€˜π»)(πΉβ€˜π΄))(+gβ€˜π»)(πΉβ€˜π΄)) = (πΉβ€˜π‘₯))
5451, 52, 45, 53syl3anc 1372 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (((πΉβ€˜π‘₯)(-gβ€˜π»)(πΉβ€˜π΄))(+gβ€˜π»)(πΉβ€˜π΄)) = (πΉβ€˜π‘₯))
5549, 54eqtrd 2773 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π΄)) = (πΉβ€˜π‘₯))
56 simprrr 781 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (πΉβ€˜π‘₯) ∈ 𝑦)
5755, 56eqeltrd 2834 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π΄)) ∈ 𝑦)
5844, 45, 57elrabd 3648 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (πΉβ€˜π΄) ∈ {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦})
59 cnpimaex 22623 . . . . . . . . . . . . 13 ((𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ∧ {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦} ∈ 𝐾 ∧ (πΉβ€˜π΄) ∈ {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦}) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ (𝐹 β€œ 𝑧) βŠ† {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦}))
6018, 42, 58, 59syl3anc 1372 . . . . . . . . . . . 12 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ (𝐹 β€œ 𝑧) βŠ† {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦}))
61 ssrab 4031 . . . . . . . . . . . . . . . 16 ((𝐹 β€œ 𝑧) βŠ† {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦} ↔ ((𝐹 β€œ 𝑧) βŠ† (Baseβ€˜π») ∧ βˆ€π‘€ ∈ (𝐹 β€œ 𝑧)((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦))
6261simprbi 498 . . . . . . . . . . . . . . 15 ((𝐹 β€œ 𝑧) βŠ† {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦} β†’ βˆ€π‘€ ∈ (𝐹 β€œ 𝑧)((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦)
6322adantr 482 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) β†’ 𝐹:π‘‹βŸΆ(Baseβ€˜π»))
6463ffnd 6670 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) β†’ 𝐹 Fn 𝑋)
658adantr 482 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
66 toponss 22292 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝑧 ∈ 𝐽) β†’ 𝑧 βŠ† 𝑋)
6765, 66sylan 581 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) β†’ 𝑧 βŠ† 𝑋)
68 oveq2 7366 . . . . . . . . . . . . . . . . . 18 (𝑀 = (πΉβ€˜π‘£) β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) = ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)))
6968eleq1d 2819 . . . . . . . . . . . . . . . . 17 (𝑀 = (πΉβ€˜π‘£) β†’ (((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦 ↔ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))
7069ralima 7189 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝑋 ∧ 𝑧 βŠ† 𝑋) β†’ (βˆ€π‘€ ∈ (𝐹 β€œ 𝑧)((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦 ↔ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))
7164, 67, 70syl2anc 585 . . . . . . . . . . . . . . 15 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) β†’ (βˆ€π‘€ ∈ (𝐹 β€œ 𝑧)((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦 ↔ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))
7262, 71imbitrid 243 . . . . . . . . . . . . . 14 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) β†’ ((𝐹 β€œ 𝑧) βŠ† {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦} β†’ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))
73 eqid 2733 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ 𝑋 ↦ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)) = (𝑀 ∈ 𝑋 ↦ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))
7473mptpreima 6191 . . . . . . . . . . . . . . . . 17 (β—‘(𝑀 ∈ 𝑋 ↦ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)) β€œ 𝑧) = {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧}
75 simpl1 1192 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐺 ∈ TopMnd)
7675ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ 𝐺 ∈ TopMnd)
7725adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ 𝐺 ∈ Grp)
7831adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ 𝐴 ∈ 𝑋)
7926adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ π‘₯ ∈ 𝑋)
805, 32grpsubcl 18832 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (𝐴(-gβ€˜πΊ)π‘₯) ∈ 𝑋)
8177, 78, 79, 80syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ (𝐴(-gβ€˜πΊ)π‘₯) ∈ 𝑋)
82 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (+gβ€˜πΊ) = (+gβ€˜πΊ)
8373, 5, 82, 4tmdlactcn 23469 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ TopMnd ∧ (𝐴(-gβ€˜πΊ)π‘₯) ∈ 𝑋) β†’ (𝑀 ∈ 𝑋 ↦ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)) ∈ (𝐽 Cn 𝐽))
8476, 81, 83syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ (𝑀 ∈ 𝑋 ↦ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)) ∈ (𝐽 Cn 𝐽))
85 simprl 770 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ 𝑧 ∈ 𝐽)
86 cnima 22632 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ 𝑋 ↦ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)) ∈ (𝐽 Cn 𝐽) ∧ 𝑧 ∈ 𝐽) β†’ (β—‘(𝑀 ∈ 𝑋 ↦ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)) β€œ 𝑧) ∈ 𝐽)
8784, 85, 86syl2anc 585 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ (β—‘(𝑀 ∈ 𝑋 ↦ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)) β€œ 𝑧) ∈ 𝐽)
8874, 87eqeltrrid 2839 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} ∈ 𝐽)
89 oveq2 7366 . . . . . . . . . . . . . . . . . 18 (𝑀 = π‘₯ β†’ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) = ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)π‘₯))
9089eleq1d 2819 . . . . . . . . . . . . . . . . 17 (𝑀 = π‘₯ β†’ (((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧 ↔ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)π‘₯) ∈ 𝑧))
915, 82, 32grpnpcan 18844 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)π‘₯) = 𝐴)
9277, 78, 79, 91syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)π‘₯) = 𝐴)
93 simprrl 780 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ 𝐴 ∈ 𝑧)
9492, 93eqeltrd 2834 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)π‘₯) ∈ 𝑧)
9590, 79, 94elrabd 3648 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ π‘₯ ∈ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧})
96 simprrr 781 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦)
97 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) β†’ (πΉβ€˜π‘£) = (πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)))
9897oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) = ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))))
9998eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) β†’ (((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦 ↔ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) ∈ 𝑦))
10099rspccv 3577 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦 β†’ (((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧 β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) ∈ 𝑦))
10196, 100syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ (((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧 β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) ∈ 𝑦))
102101adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ (((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧 β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) ∈ 𝑦))
10323adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ 𝐹 ∈ (𝐺 GrpHom 𝐻))
10434adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ (π‘₯(-gβ€˜πΊ)𝐴) ∈ 𝑋)
105103, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ 𝐺 ∈ Grp)
10631adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ 𝐴 ∈ 𝑋)
10726adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
108105, 106, 107, 80syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ (𝐴(-gβ€˜πΊ)π‘₯) ∈ 𝑋)
109 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ 𝑀 ∈ 𝑋)
1105, 82grpcl 18761 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ Grp ∧ (𝐴(-gβ€˜πΊ)π‘₯) ∈ 𝑋 ∧ 𝑀 ∈ 𝑋) β†’ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑋)
111105, 108, 109, 110syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑋)
1125, 82, 36ghmlin 19018 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ (π‘₯(-gβ€˜πΊ)𝐴) ∈ 𝑋 ∧ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑋) β†’ (πΉβ€˜((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) = ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))))
113103, 104, 111, 112syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ (πΉβ€˜((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) = ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))))
114 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (invgβ€˜πΊ) = (invgβ€˜πΊ)
1155, 32, 114grpinvsub 18834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ π‘₯ ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) β†’ ((invgβ€˜πΊ)β€˜(π‘₯(-gβ€˜πΊ)𝐴)) = (𝐴(-gβ€˜πΊ)π‘₯))
116105, 107, 106, 115syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ ((invgβ€˜πΊ)β€˜(π‘₯(-gβ€˜πΊ)𝐴)) = (𝐴(-gβ€˜πΊ)π‘₯))
117116oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ ((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)((invgβ€˜πΊ)β€˜(π‘₯(-gβ€˜πΊ)𝐴))) = ((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)(𝐴(-gβ€˜πΊ)π‘₯)))
118 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0gβ€˜πΊ) = (0gβ€˜πΊ)
1195, 82, 118, 114grprinv 18806 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ∈ Grp ∧ (π‘₯(-gβ€˜πΊ)𝐴) ∈ 𝑋) β†’ ((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)((invgβ€˜πΊ)β€˜(π‘₯(-gβ€˜πΊ)𝐴))) = (0gβ€˜πΊ))
120105, 104, 119syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ ((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)((invgβ€˜πΊ)β€˜(π‘₯(-gβ€˜πΊ)𝐴))) = (0gβ€˜πΊ))
121117, 120eqtr3d 2775 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ ((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)(𝐴(-gβ€˜πΊ)π‘₯)) = (0gβ€˜πΊ))
122121oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ (((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)(𝐴(-gβ€˜πΊ)π‘₯))(+gβ€˜πΊ)𝑀) = ((0gβ€˜πΊ)(+gβ€˜πΊ)𝑀))
1235, 82grpass 18762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ Grp ∧ ((π‘₯(-gβ€˜πΊ)𝐴) ∈ 𝑋 ∧ (𝐴(-gβ€˜πΊ)π‘₯) ∈ 𝑋 ∧ 𝑀 ∈ 𝑋)) β†’ (((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)(𝐴(-gβ€˜πΊ)π‘₯))(+gβ€˜πΊ)𝑀) = ((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)))
124105, 104, 108, 109, 123syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ (((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)(𝐴(-gβ€˜πΊ)π‘₯))(+gβ€˜πΊ)𝑀) = ((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)))
1255, 82, 118grplid 18785 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ Grp ∧ 𝑀 ∈ 𝑋) β†’ ((0gβ€˜πΊ)(+gβ€˜πΊ)𝑀) = 𝑀)
126105, 109, 125syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ ((0gβ€˜πΊ)(+gβ€˜πΊ)𝑀) = 𝑀)
127122, 124, 1263eqtr3d 2781 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ ((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀)) = 𝑀)
128127fveq2d 6847 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ (πΉβ€˜((π‘₯(-gβ€˜πΊ)𝐴)(+gβ€˜πΊ)((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) = (πΉβ€˜π‘€))
129113, 128eqtr3d 2775 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) = (πΉβ€˜π‘€))
130129adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) = (πΉβ€˜π‘€))
131130eleq1d 2819 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ (((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀))) ∈ 𝑦 ↔ (πΉβ€˜π‘€) ∈ 𝑦))
132102, 131sylibd 238 . . . . . . . . . . . . . . . . . . 19 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) ∧ 𝑀 ∈ 𝑋) β†’ (((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧 β†’ (πΉβ€˜π‘€) ∈ 𝑦))
133132ralrimiva 3140 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ βˆ€π‘€ ∈ 𝑋 (((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧 β†’ (πΉβ€˜π‘€) ∈ 𝑦))
134 fveq2 6843 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑀 β†’ (πΉβ€˜π‘£) = (πΉβ€˜π‘€))
135134eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑀 β†’ ((πΉβ€˜π‘£) ∈ 𝑦 ↔ (πΉβ€˜π‘€) ∈ 𝑦))
136135ralrab2 3657 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘£ ∈ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} (πΉβ€˜π‘£) ∈ 𝑦 ↔ βˆ€π‘€ ∈ 𝑋 (((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧 β†’ (πΉβ€˜π‘€) ∈ 𝑦))
137133, 136sylibr 233 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ βˆ€π‘£ ∈ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} (πΉβ€˜π‘£) ∈ 𝑦)
13822adantr 482 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ 𝐹:π‘‹βŸΆ(Baseβ€˜π»))
139138ffund 6673 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ Fun 𝐹)
140 ssrab2 4038 . . . . . . . . . . . . . . . . . . 19 {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} βŠ† 𝑋
141138fdmd 6680 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ dom 𝐹 = 𝑋)
142140, 141sseqtrrid 3998 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} βŠ† dom 𝐹)
143 funimass4 6908 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐹 ∧ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} βŠ† dom 𝐹) β†’ ((𝐹 β€œ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧}) βŠ† 𝑦 ↔ βˆ€π‘£ ∈ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} (πΉβ€˜π‘£) ∈ 𝑦))
144139, 142, 143syl2anc 585 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ ((𝐹 β€œ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧}) βŠ† 𝑦 ↔ βˆ€π‘£ ∈ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} (πΉβ€˜π‘£) ∈ 𝑦))
145137, 144mpbird 257 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ (𝐹 β€œ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧}) βŠ† 𝑦)
146 eleq2 2823 . . . . . . . . . . . . . . . . . 18 (𝑒 = {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} β†’ (π‘₯ ∈ 𝑒 ↔ π‘₯ ∈ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧}))
147 imaeq2 6010 . . . . . . . . . . . . . . . . . . 19 (𝑒 = {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} β†’ (𝐹 β€œ 𝑒) = (𝐹 β€œ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧}))
148147sseq1d 3976 . . . . . . . . . . . . . . . . . 18 (𝑒 = {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} β†’ ((𝐹 β€œ 𝑒) βŠ† 𝑦 ↔ (𝐹 β€œ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧}) βŠ† 𝑦))
149146, 148anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑒 = {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} β†’ ((π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦) ↔ (π‘₯ ∈ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} ∧ (𝐹 β€œ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧}) βŠ† 𝑦)))
150149rspcev 3580 . . . . . . . . . . . . . . . 16 (({𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} ∈ 𝐽 ∧ (π‘₯ ∈ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧} ∧ (𝐹 β€œ {𝑀 ∈ 𝑋 ∣ ((𝐴(-gβ€˜πΊ)π‘₯)(+gβ€˜πΊ)𝑀) ∈ 𝑧}) βŠ† 𝑦)) β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦))
15188, 95, 145, 150syl12anc 836 . . . . . . . . . . . . . . 15 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦))) β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦))
152151expr 458 . . . . . . . . . . . . . 14 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) β†’ ((𝐴 ∈ 𝑧 ∧ βˆ€π‘£ ∈ 𝑧 ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)(πΉβ€˜π‘£)) ∈ 𝑦) β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦)))
15372, 152sylan2d 606 . . . . . . . . . . . . 13 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) β†’ ((𝐴 ∈ 𝑧 ∧ (𝐹 β€œ 𝑧) βŠ† {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦}) β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦)))
154153rexlimdva 3149 . . . . . . . . . . . 12 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ (βˆƒπ‘§ ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ (𝐹 β€œ 𝑧) βŠ† {𝑀 ∈ (Baseβ€˜π») ∣ ((πΉβ€˜(π‘₯(-gβ€˜πΊ)𝐴))(+gβ€˜π»)𝑀) ∈ 𝑦}) β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦)))
15560, 154mpd 15 . . . . . . . . . . 11 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ (π‘₯ ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦))) β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦))
156155anassrs 469 . . . . . . . . . 10 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ π‘₯ ∈ 𝑋) ∧ (𝑦 ∈ 𝐾 ∧ (πΉβ€˜π‘₯) ∈ 𝑦)) β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦))
157156expr 458 . . . . . . . . 9 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ π‘₯ ∈ 𝑋) ∧ 𝑦 ∈ 𝐾) β†’ ((πΉβ€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦)))
158157ralrimiva 3140 . . . . . . . 8 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ π‘₯ ∈ 𝑋) β†’ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦)))
1598adantr 482 . . . . . . . . 9 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ π‘₯ ∈ 𝑋) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
16013adantr 482 . . . . . . . . 9 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ π‘₯ ∈ 𝑋) β†’ 𝐾 ∈ (TopOnβ€˜(Baseβ€˜π»)))
161 simpr 486 . . . . . . . . 9 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
162 iscnp 22604 . . . . . . . . 9 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜(Baseβ€˜π»)) ∧ π‘₯ ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘₯) ↔ (𝐹:π‘‹βŸΆ(Baseβ€˜π») ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦)))))
163159, 160, 161, 162syl3anc 1372 . . . . . . . 8 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ π‘₯ ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘₯) ↔ (𝐹:π‘‹βŸΆ(Baseβ€˜π») ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘’ ∈ 𝐽 (π‘₯ ∈ 𝑒 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑦)))))
16417, 158, 163mpbir2and 712 . . . . . . 7 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) ∧ π‘₯ ∈ 𝑋) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘₯))
165164ralrimiva 3140 . . . . . 6 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ βˆ€π‘₯ ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘₯))
166 cncnp 22647 . . . . . . 7 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜(Baseβ€˜π»))) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:π‘‹βŸΆ(Baseβ€˜π») ∧ βˆ€π‘₯ ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘₯))))
1678, 13, 166syl2anc 585 . . . . . 6 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:π‘‹βŸΆ(Baseβ€˜π») ∧ βˆ€π‘₯ ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘₯))))
16816, 165, 167mpbir2and 712 . . . . 5 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄)) β†’ 𝐹 ∈ (𝐽 Cn 𝐾))
169168ex 414 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) β†’ 𝐹 ∈ (𝐽 Cn 𝐾)))
1703, 169jcad 514 . . 3 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) β†’ (𝐴 ∈ βˆͺ 𝐽 ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))
1711cncnpi 22645 . . . 4 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ βˆͺ 𝐽) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄))
172171ancoms 460 . . 3 ((𝐴 ∈ βˆͺ 𝐽 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄))
173170, 172impbid1 224 . 2 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ (𝐴 ∈ βˆͺ 𝐽 ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))
1747, 28syl 17 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ 𝑋 = βˆͺ 𝐽)
175174eleq2d 2820 . . 3 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ βˆͺ 𝐽))
176175anbi1d 631 . 2 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ ((𝐴 ∈ 𝑋 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ↔ (𝐴 ∈ βˆͺ 𝐽 ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))
177173, 176bitr4d 282 1 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ (𝐴 ∈ 𝑋 ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406   βŠ† wss 3911  βˆͺ cuni 4866   ↦ cmpt 5189  β—‘ccnv 5633  dom cdm 5634   β€œ cima 5637  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358  Basecbs 17088  +gcplusg 17138  TopOpenctopn 17308  0gc0g 17326  Grpcgrp 18753  invgcminusg 18754  -gcsg 18755   GrpHom cghm 19010  TopOnctopon 22275   Cn ccn 22591   CnP ccnp 22592  TopMndctmd 23437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-map 8770  df-0g 17328  df-topgen 17330  df-plusf 18501  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-grp 18756  df-minusg 18757  df-sbg 18758  df-ghm 19011  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cn 22594  df-cnp 22595  df-tx 22929  df-tmd 23439
This theorem is referenced by:  qqhcn  32629
  Copyright terms: Public domain W3C validator