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

Theorem ghmcnp 23372
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 2736 . . . . . 6 𝐽 = 𝐽
21cnprcl 22502 . . . . 5 (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐴 𝐽)
32a1i 11 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐴 𝐽))
4 ghmcnp.j . . . . . . . . . 10 𝐽 = (TopOpen‘𝐺)
5 ghmcnp.x . . . . . . . . . 10 𝑋 = (Base‘𝐺)
64, 5tmdtopon 23338 . . . . . . . . 9 (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝑋))
763ad2ant1 1132 . . . . . . . 8 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → 𝐽 ∈ (TopOn‘𝑋))
87adantr 481 . . . . . . 7 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
9 simpl2 1191 . . . . . . . 8 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐻 ∈ TopMnd)
10 ghmcnp.k . . . . . . . . 9 𝐾 = (TopOpen‘𝐻)
11 eqid 2736 . . . . . . . . 9 (Base‘𝐻) = (Base‘𝐻)
1210, 11tmdtopon 23338 . . . . . . . 8 (𝐻 ∈ TopMnd → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
139, 12syl 17 . . . . . . 7 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
14 simpr 485 . . . . . . 7 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
15 cnpf2 22507 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶(Base‘𝐻))
168, 13, 14, 15syl3anc 1370 . . . . . 6 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶(Base‘𝐻))
1716adantr 481 . . . . . . . 8 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝐹:𝑋⟶(Base‘𝐻))
1814adantr 481 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
19 eqid 2736 . . . . . . . . . . . . . . 15 (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) = (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤))
2019mptpreima 6176 . . . . . . . . . . . . . 14 ((𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) “ 𝑦) = {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}
219adantr 481 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐻 ∈ TopMnd)
2216adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐹:𝑋⟶(Base‘𝐻))
23 simpll3 1213 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
24 ghmgrp1 18932 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp)
2523, 24syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐺 ∈ Grp)
26 simprl 768 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝑥𝑋)
272adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐴 𝐽)
28 toponuni 22169 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
298, 28syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝑋 = 𝐽)
3027, 29eleqtrrd 2840 . . . . . . . . . . . . . . . . . . 19 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐴𝑋)
3130adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐴𝑋)
32 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (-g𝐺) = (-g𝐺)
335, 32grpsubcl 18751 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ 𝑥𝑋𝐴𝑋) → (𝑥(-g𝐺)𝐴) ∈ 𝑋)
3425, 26, 31, 33syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝑥(-g𝐺)𝐴) ∈ 𝑋)
3522, 34ffvelcdmd 7018 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹‘(𝑥(-g𝐺)𝐴)) ∈ (Base‘𝐻))
36 eqid 2736 . . . . . . . . . . . . . . . . 17 (+g𝐻) = (+g𝐻)
3719, 11, 36, 10tmdlactcn 23359 . . . . . . . . . . . . . . . 16 ((𝐻 ∈ TopMnd ∧ (𝐹‘(𝑥(-g𝐺)𝐴)) ∈ (Base‘𝐻)) → (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) ∈ (𝐾 Cn 𝐾))
3821, 35, 37syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) ∈ (𝐾 Cn 𝐾))
39 simprrl 778 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝑦𝐾)
40 cnima 22522 . . . . . . . . . . . . . . 15 (((𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) ∈ (𝐾 Cn 𝐾) ∧ 𝑦𝐾) → ((𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) “ 𝑦) ∈ 𝐾)
4138, 39, 40syl2anc 584 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ((𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) “ 𝑦) ∈ 𝐾)
4220, 41eqeltrrid 2842 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} ∈ 𝐾)
43 oveq2 7345 . . . . . . . . . . . . . . 15 (𝑤 = (𝐹𝐴) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)))
4443eleq1d 2821 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝐴) → (((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦 ↔ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)) ∈ 𝑦))
4522, 31ffvelcdmd 7018 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹𝐴) ∈ (Base‘𝐻))
46 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (-g𝐻) = (-g𝐻)
475, 32, 46ghmsub 18938 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥𝑋𝐴𝑋) → (𝐹‘(𝑥(-g𝐺)𝐴)) = ((𝐹𝑥)(-g𝐻)(𝐹𝐴)))
4823, 26, 31, 47syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹‘(𝑥(-g𝐺)𝐴)) = ((𝐹𝑥)(-g𝐻)(𝐹𝐴)))
4948oveq1d 7352 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)) = (((𝐹𝑥)(-g𝐻)(𝐹𝐴))(+g𝐻)(𝐹𝐴)))
50 ghmgrp2 18933 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp)
5123, 50syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐻 ∈ Grp)
5222, 26ffvelcdmd 7018 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹𝑥) ∈ (Base‘𝐻))
5311, 36, 46grpnpcan 18763 . . . . . . . . . . . . . . . . 17 ((𝐻 ∈ Grp ∧ (𝐹𝑥) ∈ (Base‘𝐻) ∧ (𝐹𝐴) ∈ (Base‘𝐻)) → (((𝐹𝑥)(-g𝐻)(𝐹𝐴))(+g𝐻)(𝐹𝐴)) = (𝐹𝑥))
5451, 52, 45, 53syl3anc 1370 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (((𝐹𝑥)(-g𝐻)(𝐹𝐴))(+g𝐻)(𝐹𝐴)) = (𝐹𝑥))
5549, 54eqtrd 2776 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)) = (𝐹𝑥))
56 simprrr 779 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹𝑥) ∈ 𝑦)
5755, 56eqeltrd 2837 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)) ∈ 𝑦)
5844, 45, 57elrabd 3636 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹𝐴) ∈ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦})
59 cnpimaex 22513 . . . . . . . . . . . . 13 ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} ∈ 𝐾 ∧ (𝐹𝐴) ∈ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}) → ∃𝑧𝐽 (𝐴𝑧 ∧ (𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}))
6018, 42, 58, 59syl3anc 1370 . . . . . . . . . . . 12 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ∃𝑧𝐽 (𝐴𝑧 ∧ (𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}))
61 ssrab 4018 . . . . . . . . . . . . . . . 16 ((𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} ↔ ((𝐹𝑧) ⊆ (Base‘𝐻) ∧ ∀𝑤 ∈ (𝐹𝑧)((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦))
6261simprbi 497 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} → ∀𝑤 ∈ (𝐹𝑧)((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦)
6322adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → 𝐹:𝑋⟶(Base‘𝐻))
6463ffnd 6652 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → 𝐹 Fn 𝑋)
658adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐽 ∈ (TopOn‘𝑋))
66 toponss 22182 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽) → 𝑧𝑋)
6765, 66sylan 580 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → 𝑧𝑋)
68 oveq2 7345 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹𝑣) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)))
6968eleq1d 2821 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐹𝑣) → (((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦 ↔ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))
7069ralima 7170 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝑋𝑧𝑋) → (∀𝑤 ∈ (𝐹𝑧)((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦 ↔ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))
7164, 67, 70syl2anc 584 . . . . . . . . . . . . . . 15 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → (∀𝑤 ∈ (𝐹𝑧)((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦 ↔ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))
7262, 71syl5ib 243 . . . . . . . . . . . . . 14 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → ((𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} → ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))
73 eqid 2736 . . . . . . . . . . . . . . . . . 18 (𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) = (𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))
7473mptpreima 6176 . . . . . . . . . . . . . . . . 17 ((𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) “ 𝑧) = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}
75 simpl1 1190 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐺 ∈ TopMnd)
7675ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐺 ∈ TopMnd)
7725adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐺 ∈ Grp)
7831adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐴𝑋)
7926adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝑥𝑋)
805, 32grpsubcl 18751 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ 𝐴𝑋𝑥𝑋) → (𝐴(-g𝐺)𝑥) ∈ 𝑋)
8177, 78, 79, 80syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → (𝐴(-g𝐺)𝑥) ∈ 𝑋)
82 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (+g𝐺) = (+g𝐺)
8373, 5, 82, 4tmdlactcn 23359 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ TopMnd ∧ (𝐴(-g𝐺)𝑥) ∈ 𝑋) → (𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) ∈ (𝐽 Cn 𝐽))
8476, 81, 83syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → (𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) ∈ (𝐽 Cn 𝐽))
85 simprl 768 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝑧𝐽)
86 cnima 22522 . . . . . . . . . . . . . . . . . 18 (((𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) ∈ (𝐽 Cn 𝐽) ∧ 𝑧𝐽) → ((𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) “ 𝑧) ∈ 𝐽)
8784, 85, 86syl2anc 584 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ((𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) “ 𝑧) ∈ 𝐽)
8874, 87eqeltrrid 2842 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ∈ 𝐽)
89 oveq2 7345 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) = ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥))
9089eleq1d 2821 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥 → (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 ↔ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥) ∈ 𝑧))
915, 82, 32grpnpcan 18763 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝐴𝑋𝑥𝑋) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥) = 𝐴)
9277, 78, 79, 91syl3anc 1370 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥) = 𝐴)
93 simprrl 778 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐴𝑧)
9492, 93eqeltrd 2837 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥) ∈ 𝑧)
9590, 79, 94elrabd 3636 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝑥 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧})
96 simprrr 779 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦)
97 fveq2 6825 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) → (𝐹𝑣) = (𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)))
9897oveq2d 7353 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))))
9998eleq1d 2821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) → (((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦 ↔ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) ∈ 𝑦))
10099rspccv 3567 . . . . . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) ∈ 𝑦))
10323adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
10434adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (𝑥(-g𝐺)𝐴) ∈ 𝑋)
105103, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝐺 ∈ Grp)
10631adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝐴𝑋)
10726adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝑥𝑋)
108105, 106, 107, 80syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (𝐴(-g𝐺)𝑥) ∈ 𝑋)
109 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝑤𝑋)
1105, 82grpcl 18681 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ Grp ∧ (𝐴(-g𝐺)𝑥) ∈ 𝑋𝑤𝑋) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑋)
111105, 108, 109, 110syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑋)
1125, 82, 36ghmlin 18935 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑥(-g𝐺)𝐴) ∈ 𝑋 ∧ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑋) → (𝐹‘((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))))
113103, 104, 111, 112syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (𝐹‘((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))))
114 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (invg𝐺) = (invg𝐺)
1155, 32, 114grpinvsub 18753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ 𝑥𝑋𝐴𝑋) → ((invg𝐺)‘(𝑥(-g𝐺)𝐴)) = (𝐴(-g𝐺)𝑥))
116105, 107, 106, 115syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((invg𝐺)‘(𝑥(-g𝐺)𝐴)) = (𝐴(-g𝐺)𝑥))
117116oveq2d 7353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)((invg𝐺)‘(𝑥(-g𝐺)𝐴))) = ((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥)))
118 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0g𝐺) = (0g𝐺)
1195, 82, 118, 114grprinv 18725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ∈ Grp ∧ (𝑥(-g𝐺)𝐴) ∈ 𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)((invg𝐺)‘(𝑥(-g𝐺)𝐴))) = (0g𝐺))
120105, 104, 119syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)((invg𝐺)‘(𝑥(-g𝐺)𝐴))) = (0g𝐺))
121117, 120eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥)) = (0g𝐺))
122121oveq1d 7352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥))(+g𝐺)𝑤) = ((0g𝐺)(+g𝐺)𝑤))
1235, 82grpass 18682 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ Grp ∧ ((𝑥(-g𝐺)𝐴) ∈ 𝑋 ∧ (𝐴(-g𝐺)𝑥) ∈ 𝑋𝑤𝑋)) → (((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥))(+g𝐺)𝑤) = ((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)))
124105, 104, 108, 109, 123syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥))(+g𝐺)𝑤) = ((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)))
1255, 82, 118grplid 18705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ Grp ∧ 𝑤𝑋) → ((0g𝐺)(+g𝐺)𝑤) = 𝑤)
126105, 109, 125syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((0g𝐺)(+g𝐺)𝑤) = 𝑤)
127122, 124, 1263eqtr3d 2784 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) = 𝑤)
128127fveq2d 6829 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (𝐹‘((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = (𝐹𝑤))
129113, 128eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = (𝐹𝑤))
130129adantlr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = (𝐹𝑤))
131130eleq1d 2821 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) ∈ 𝑦 ↔ (𝐹𝑤) ∈ 𝑦))
132102, 131sylibd 238 . . . . . . . . . . . . . . . . . . 19 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 → (𝐹𝑤) ∈ 𝑦))
133132ralrimiva 3139 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ∀𝑤𝑋 (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 → (𝐹𝑤) ∈ 𝑦))
134 fveq2 6825 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑤 → (𝐹𝑣) = (𝐹𝑤))
135134eleq1d 2821 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → ((𝐹𝑣) ∈ 𝑦 ↔ (𝐹𝑤) ∈ 𝑦))
136135ralrab2 3645 . . . . . . . . . . . . . . . . . 18 (∀𝑣 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} (𝐹𝑣) ∈ 𝑦 ↔ ∀𝑤𝑋 (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 → (𝐹𝑤) ∈ 𝑦))
137133, 136sylibr 233 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ∀𝑣 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} (𝐹𝑣) ∈ 𝑦)
13822adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐹:𝑋⟶(Base‘𝐻))
139138ffund 6655 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → Fun 𝐹)
140 ssrab2 4025 . . . . . . . . . . . . . . . . . . 19 {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ⊆ 𝑋
141138fdmd 6662 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → dom 𝐹 = 𝑋)
142140, 141sseqtrrid 3985 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ⊆ dom 𝐹)
143 funimass4 6890 . . . . . . . . . . . . . . . . . 18 ((Fun 𝐹 ∧ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ⊆ dom 𝐹) → ((𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦 ↔ ∀𝑣 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} (𝐹𝑣) ∈ 𝑦))
144139, 142, 143syl2anc 584 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ((𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦 ↔ ∀𝑣 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} (𝐹𝑣) ∈ 𝑦))
145137, 144mpbird 256 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦)
146 eleq2 2825 . . . . . . . . . . . . . . . . . 18 (𝑢 = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} → (𝑥𝑢𝑥 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}))
147 imaeq2 5995 . . . . . . . . . . . . . . . . . . 19 (𝑢 = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} → (𝐹𝑢) = (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}))
148147sseq1d 3963 . . . . . . . . . . . . . . . . . 18 (𝑢 = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} → ((𝐹𝑢) ⊆ 𝑦 ↔ (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦))
149146, 148anbi12d 631 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} → ((𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦) ↔ (𝑥 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ∧ (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦)))
150149rspcev 3570 . . . . . . . . . . . . . . . 16 (({𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ∈ 𝐽 ∧ (𝑥 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ∧ (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦)) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
15188, 95, 145, 150syl12anc 834 . . . . . . . . . . . . . . 15 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
152151expr 457 . . . . . . . . . . . . . 14 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → ((𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
15372, 152sylan2d 605 . . . . . . . . . . . . 13 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → ((𝐴𝑧 ∧ (𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
154153rexlimdva 3148 . . . . . . . . . . . 12 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (∃𝑧𝐽 (𝐴𝑧 ∧ (𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
15560, 154mpd 15 . . . . . . . . . . 11 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
156155anassrs 468 . . . . . . . . . 10 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦)) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
157156expr 457 . . . . . . . . 9 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) ∧ 𝑦𝐾) → ((𝐹𝑥) ∈ 𝑦 → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
158157ralrimiva 3139 . . . . . . . 8 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → ∀𝑦𝐾 ((𝐹𝑥) ∈ 𝑦 → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
1598adantr 481 . . . . . . . . 9 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝐽 ∈ (TopOn‘𝑋))
16013adantr 481 . . . . . . . . 9 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
161 simpr 485 . . . . . . . . 9 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝑥𝑋)
162 iscnp 22494 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝑥𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑦𝐾 ((𝐹𝑥) ∈ 𝑦 → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))))
163159, 160, 161, 162syl3anc 1370 . . . . . . . 8 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑦𝐾 ((𝐹𝑥) ∈ 𝑦 → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))))
16417, 158, 163mpbir2and 710 . . . . . . 7 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
165164ralrimiva 3139 . . . . . 6 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
166 cncnp 22537 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
1678, 13, 166syl2anc 584 . . . . . 6 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
16816, 165, 167mpbir2and 710 . . . . 5 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹 ∈ (𝐽 Cn 𝐾))
169168ex 413 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐹 ∈ (𝐽 Cn 𝐾)))
1703, 169jcad 513 . . 3 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝐴 𝐽𝐹 ∈ (𝐽 Cn 𝐾))))
1711cncnpi 22535 . . . 4 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 𝐽) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
172171ancoms 459 . . 3 ((𝐴 𝐽𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
173170, 172impbid1 224 . 2 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐴 𝐽𝐹 ∈ (𝐽 Cn 𝐾))))
1747, 28syl 17 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → 𝑋 = 𝐽)
175174eleq2d 2822 . . 3 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐴𝑋𝐴 𝐽))
176175anbi1d 630 . 2 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → ((𝐴𝑋𝐹 ∈ (𝐽 Cn 𝐾)) ↔ (𝐴 𝐽𝐹 ∈ (𝐽 Cn 𝐾))))
177173, 176bitr4d 281 1 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐴𝑋𝐹 ∈ (𝐽 Cn 𝐾))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wral 3061  wrex 3070  {crab 3403  wss 3898   cuni 4852  cmpt 5175  ccnv 5619  dom cdm 5620  cima 5623  Fun wfun 6473   Fn wfn 6474  wf 6475  cfv 6479  (class class class)co 7337  Basecbs 17009  +gcplusg 17059  TopOpenctopn 17229  0gc0g 17247  Grpcgrp 18673  invgcminusg 18674  -gcsg 18675   GrpHom cghm 18927  TopOnctopon 22165   Cn ccn 22481   CnP ccnp 22482  TopMndctmd 23327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-1st 7899  df-2nd 7900  df-map 8688  df-0g 17249  df-topgen 17251  df-plusf 18422  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-grp 18676  df-minusg 18677  df-sbg 18678  df-ghm 18928  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cn 22484  df-cnp 22485  df-tx 22819  df-tmd 23329
This theorem is referenced by:  qqhcn  32239
  Copyright terms: Public domain W3C validator