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

Theorem ghmcnp 24123
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 2737 . . . . . 6 𝐽 = 𝐽
21cnprcl 23253 . . . . 5 (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐴 𝐽)
32a1i 11 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐴 𝐽))
4 ghmcnp.j . . . . . . . . . 10 𝐽 = (TopOpen‘𝐺)
5 ghmcnp.x . . . . . . . . . 10 𝑋 = (Base‘𝐺)
64, 5tmdtopon 24089 . . . . . . . . 9 (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝑋))
763ad2ant1 1134 . . . . . . . 8 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → 𝐽 ∈ (TopOn‘𝑋))
87adantr 480 . . . . . . 7 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
9 simpl2 1193 . . . . . . . 8 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐻 ∈ TopMnd)
10 ghmcnp.k . . . . . . . . 9 𝐾 = (TopOpen‘𝐻)
11 eqid 2737 . . . . . . . . 9 (Base‘𝐻) = (Base‘𝐻)
1210, 11tmdtopon 24089 . . . . . . . 8 (𝐻 ∈ TopMnd → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
139, 12syl 17 . . . . . . 7 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
14 simpr 484 . . . . . . 7 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
15 cnpf2 23258 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶(Base‘𝐻))
168, 13, 14, 15syl3anc 1373 . . . . . 6 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶(Base‘𝐻))
1716adantr 480 . . . . . . . 8 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝐹:𝑋⟶(Base‘𝐻))
1814adantr 480 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
19 eqid 2737 . . . . . . . . . . . . . . 15 (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) = (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤))
2019mptpreima 6258 . . . . . . . . . . . . . 14 ((𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) “ 𝑦) = {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}
219adantr 480 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐻 ∈ TopMnd)
2216adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐹:𝑋⟶(Base‘𝐻))
23 simpll3 1215 . . . . . . . . . . . . . . . . . . 19 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
24 ghmgrp1 19236 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp)
2523, 24syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐺 ∈ Grp)
26 simprl 771 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝑥𝑋)
272adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐴 𝐽)
28 toponuni 22920 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
298, 28syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝑋 = 𝐽)
3027, 29eleqtrrd 2844 . . . . . . . . . . . . . . . . . . 19 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐴𝑋)
3130adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐴𝑋)
32 eqid 2737 . . . . . . . . . . . . . . . . . . 19 (-g𝐺) = (-g𝐺)
335, 32grpsubcl 19038 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ 𝑥𝑋𝐴𝑋) → (𝑥(-g𝐺)𝐴) ∈ 𝑋)
3425, 26, 31, 33syl3anc 1373 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝑥(-g𝐺)𝐴) ∈ 𝑋)
3522, 34ffvelcdmd 7105 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹‘(𝑥(-g𝐺)𝐴)) ∈ (Base‘𝐻))
36 eqid 2737 . . . . . . . . . . . . . . . . 17 (+g𝐻) = (+g𝐻)
3719, 11, 36, 10tmdlactcn 24110 . . . . . . . . . . . . . . . 16 ((𝐻 ∈ TopMnd ∧ (𝐹‘(𝑥(-g𝐺)𝐴)) ∈ (Base‘𝐻)) → (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) ∈ (𝐾 Cn 𝐾))
3821, 35, 37syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) ∈ (𝐾 Cn 𝐾))
39 simprrl 781 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝑦𝐾)
40 cnima 23273 . . . . . . . . . . . . . . 15 (((𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) ∈ (𝐾 Cn 𝐾) ∧ 𝑦𝐾) → ((𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) “ 𝑦) ∈ 𝐾)
4138, 39, 40syl2anc 584 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ((𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤)) “ 𝑦) ∈ 𝐾)
4220, 41eqeltrrid 2846 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} ∈ 𝐾)
43 oveq2 7439 . . . . . . . . . . . . . . 15 (𝑤 = (𝐹𝐴) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)))
4443eleq1d 2826 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝐴) → (((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦 ↔ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)) ∈ 𝑦))
4522, 31ffvelcdmd 7105 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹𝐴) ∈ (Base‘𝐻))
46 eqid 2737 . . . . . . . . . . . . . . . . . . 19 (-g𝐻) = (-g𝐻)
475, 32, 46ghmsub 19242 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥𝑋𝐴𝑋) → (𝐹‘(𝑥(-g𝐺)𝐴)) = ((𝐹𝑥)(-g𝐻)(𝐹𝐴)))
4823, 26, 31, 47syl3anc 1373 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹‘(𝑥(-g𝐺)𝐴)) = ((𝐹𝑥)(-g𝐻)(𝐹𝐴)))
4948oveq1d 7446 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)) = (((𝐹𝑥)(-g𝐻)(𝐹𝐴))(+g𝐻)(𝐹𝐴)))
50 ghmgrp2 19237 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp)
5123, 50syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐻 ∈ Grp)
5222, 26ffvelcdmd 7105 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹𝑥) ∈ (Base‘𝐻))
5311, 36, 46grpnpcan 19050 . . . . . . . . . . . . . . . . 17 ((𝐻 ∈ Grp ∧ (𝐹𝑥) ∈ (Base‘𝐻) ∧ (𝐹𝐴) ∈ (Base‘𝐻)) → (((𝐹𝑥)(-g𝐻)(𝐹𝐴))(+g𝐻)(𝐹𝐴)) = (𝐹𝑥))
5451, 52, 45, 53syl3anc 1373 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (((𝐹𝑥)(-g𝐻)(𝐹𝐴))(+g𝐻)(𝐹𝐴)) = (𝐹𝑥))
5549, 54eqtrd 2777 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)) = (𝐹𝑥))
56 simprrr 782 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹𝑥) ∈ 𝑦)
5755, 56eqeltrd 2841 . . . . . . . . . . . . . 14 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝐴)) ∈ 𝑦)
5844, 45, 57elrabd 3694 . . . . . . . . . . . . 13 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (𝐹𝐴) ∈ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦})
59 cnpimaex 23264 . . . . . . . . . . . . 13 ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} ∈ 𝐾 ∧ (𝐹𝐴) ∈ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}) → ∃𝑧𝐽 (𝐴𝑧 ∧ (𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}))
6018, 42, 58, 59syl3anc 1373 . . . . . . . . . . . 12 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ∃𝑧𝐽 (𝐴𝑧 ∧ (𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}))
61 ssrab 4073 . . . . . . . . . . . . . . . 16 ((𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} ↔ ((𝐹𝑧) ⊆ (Base‘𝐻) ∧ ∀𝑤 ∈ (𝐹𝑧)((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦))
6261simprbi 496 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} → ∀𝑤 ∈ (𝐹𝑧)((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦)
6322adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → 𝐹:𝑋⟶(Base‘𝐻))
6463ffnd 6737 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → 𝐹 Fn 𝑋)
658adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → 𝐽 ∈ (TopOn‘𝑋))
66 toponss 22933 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽) → 𝑧𝑋)
6765, 66sylan 580 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → 𝑧𝑋)
68 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹𝑣) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)))
6968eleq1d 2826 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐹𝑣) → (((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦 ↔ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))
7069ralima 7257 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝑋𝑧𝑋) → (∀𝑤 ∈ (𝐹𝑧)((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦 ↔ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))
7164, 67, 70syl2anc 584 . . . . . . . . . . . . . . 15 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → (∀𝑤 ∈ (𝐹𝑧)((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦 ↔ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))
7262, 71imbitrid 244 . . . . . . . . . . . . . 14 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → ((𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦} → ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))
73 eqid 2737 . . . . . . . . . . . . . . . . . 18 (𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) = (𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))
7473mptpreima 6258 . . . . . . . . . . . . . . . . 17 ((𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) “ 𝑧) = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}
75 simpl1 1192 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐺 ∈ TopMnd)
7675ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐺 ∈ TopMnd)
7725adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐺 ∈ Grp)
7831adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐴𝑋)
7926adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝑥𝑋)
805, 32grpsubcl 19038 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ 𝐴𝑋𝑥𝑋) → (𝐴(-g𝐺)𝑥) ∈ 𝑋)
8177, 78, 79, 80syl3anc 1373 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → (𝐴(-g𝐺)𝑥) ∈ 𝑋)
82 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (+g𝐺) = (+g𝐺)
8373, 5, 82, 4tmdlactcn 24110 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ TopMnd ∧ (𝐴(-g𝐺)𝑥) ∈ 𝑋) → (𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) ∈ (𝐽 Cn 𝐽))
8476, 81, 83syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → (𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) ∈ (𝐽 Cn 𝐽))
85 simprl 771 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝑧𝐽)
86 cnima 23273 . . . . . . . . . . . . . . . . . 18 (((𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) ∈ (𝐽 Cn 𝐽) ∧ 𝑧𝐽) → ((𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) “ 𝑧) ∈ 𝐽)
8784, 85, 86syl2anc 584 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ((𝑤𝑋 ↦ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) “ 𝑧) ∈ 𝐽)
8874, 87eqeltrrid 2846 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ∈ 𝐽)
89 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) = ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥))
9089eleq1d 2826 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥 → (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 ↔ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥) ∈ 𝑧))
915, 82, 32grpnpcan 19050 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝐴𝑋𝑥𝑋) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥) = 𝐴)
9277, 78, 79, 91syl3anc 1373 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥) = 𝐴)
93 simprrl 781 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐴𝑧)
9492, 93eqeltrd 2841 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑥) ∈ 𝑧)
9590, 79, 94elrabd 3694 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝑥 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧})
96 simprrr 782 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦)
97 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) → (𝐹𝑣) = (𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)))
9897oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))))
9998eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) → (((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦 ↔ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) ∈ 𝑦))
10099rspccv 3619 . . . . . . . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) ∈ 𝑦))
10323adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
10434adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (𝑥(-g𝐺)𝐴) ∈ 𝑋)
105103, 24syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝐺 ∈ Grp)
10631adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝐴𝑋)
10726adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝑥𝑋)
108105, 106, 107, 80syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (𝐴(-g𝐺)𝑥) ∈ 𝑋)
109 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → 𝑤𝑋)
1105, 82grpcl 18959 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ Grp ∧ (𝐴(-g𝐺)𝑥) ∈ 𝑋𝑤𝑋) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑋)
111105, 108, 109, 110syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑋)
1125, 82, 36ghmlin 19239 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑥(-g𝐺)𝐴) ∈ 𝑋 ∧ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑋) → (𝐹‘((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))))
113103, 104, 111, 112syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (𝐹‘((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))))
114 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (invg𝐺) = (invg𝐺)
1155, 32, 114grpinvsub 19040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ 𝑥𝑋𝐴𝑋) → ((invg𝐺)‘(𝑥(-g𝐺)𝐴)) = (𝐴(-g𝐺)𝑥))
116105, 107, 106, 115syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((invg𝐺)‘(𝑥(-g𝐺)𝐴)) = (𝐴(-g𝐺)𝑥))
117116oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)((invg𝐺)‘(𝑥(-g𝐺)𝐴))) = ((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥)))
118 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (0g𝐺) = (0g𝐺)
1195, 82, 118, 114grprinv 19008 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ∈ Grp ∧ (𝑥(-g𝐺)𝐴) ∈ 𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)((invg𝐺)‘(𝑥(-g𝐺)𝐴))) = (0g𝐺))
120105, 104, 119syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)((invg𝐺)‘(𝑥(-g𝐺)𝐴))) = (0g𝐺))
121117, 120eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥)) = (0g𝐺))
122121oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥))(+g𝐺)𝑤) = ((0g𝐺)(+g𝐺)𝑤))
1235, 82grpass 18960 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ Grp ∧ ((𝑥(-g𝐺)𝐴) ∈ 𝑋 ∧ (𝐴(-g𝐺)𝑥) ∈ 𝑋𝑤𝑋)) → (((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥))(+g𝐺)𝑤) = ((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)))
124105, 104, 108, 109, 123syl13anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝑥(-g𝐺)𝐴)(+g𝐺)(𝐴(-g𝐺)𝑥))(+g𝐺)𝑤) = ((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)))
1255, 82, 118grplid 18985 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ Grp ∧ 𝑤𝑋) → ((0g𝐺)(+g𝐺)𝑤) = 𝑤)
126105, 109, 125syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((0g𝐺)(+g𝐺)𝑤) = 𝑤)
127122, 124, 1263eqtr3d 2785 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤)) = 𝑤)
128127fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → (𝐹‘((𝑥(-g𝐺)𝐴)(+g𝐺)((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = (𝐹𝑤))
129113, 128eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = (𝐹𝑤))
130129adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) ∧ 𝑤𝑋) → ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) = (𝐹𝑤))
131130eleq1d 2826 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹‘((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤))) ∈ 𝑦 ↔ (𝐹𝑤) ∈ 𝑦))
132102, 131sylibd 239 . . . . . . . . . . . . . . . . . . 19 ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) ∧ 𝑤𝑋) → (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 → (𝐹𝑤) ∈ 𝑦))
133132ralrimiva 3146 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ∀𝑤𝑋 (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 → (𝐹𝑤) ∈ 𝑦))
134 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑤 → (𝐹𝑣) = (𝐹𝑤))
135134eleq1d 2826 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑤 → ((𝐹𝑣) ∈ 𝑦 ↔ (𝐹𝑤) ∈ 𝑦))
136135ralrab2 3704 . . . . . . . . . . . . . . . . . 18 (∀𝑣 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} (𝐹𝑣) ∈ 𝑦 ↔ ∀𝑤𝑋 (((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧 → (𝐹𝑤) ∈ 𝑦))
137133, 136sylibr 234 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ∀𝑣 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} (𝐹𝑣) ∈ 𝑦)
13822adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → 𝐹:𝑋⟶(Base‘𝐻))
139138ffund 6740 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → Fun 𝐹)
140 ssrab2 4080 . . . . . . . . . . . . . . . . . . 19 {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ⊆ 𝑋
141138fdmd 6746 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → dom 𝐹 = 𝑋)
142140, 141sseqtrrid 4027 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ⊆ dom 𝐹)
143 funimass4 6973 . . . . . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦)
146 eleq2 2830 . . . . . . . . . . . . . . . . . 18 (𝑢 = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} → (𝑥𝑢𝑥 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}))
147 imaeq2 6074 . . . . . . . . . . . . . . . . . . 19 (𝑢 = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} → (𝐹𝑢) = (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}))
148147sseq1d 4015 . . . . . . . . . . . . . . . . . 18 (𝑢 = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} → ((𝐹𝑢) ⊆ 𝑦 ↔ (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦))
149146, 148anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑢 = {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} → ((𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦) ↔ (𝑥 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ∧ (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦)))
150149rspcev 3622 . . . . . . . . . . . . . . . 16 (({𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ∈ 𝐽 ∧ (𝑥 ∈ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧} ∧ (𝐹 “ {𝑤𝑋 ∣ ((𝐴(-g𝐺)𝑥)(+g𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦)) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
15188, 95, 145, 150syl12anc 837 . . . . . . . . . . . . . . 15 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ (𝑧𝐽 ∧ (𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦))) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
152151expr 456 . . . . . . . . . . . . . 14 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → ((𝐴𝑧 ∧ ∀𝑣𝑧 ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)(𝐹𝑣)) ∈ 𝑦) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
15372, 152sylan2d 605 . . . . . . . . . . . . 13 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) ∧ 𝑧𝐽) → ((𝐴𝑧 ∧ (𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
154153rexlimdva 3155 . . . . . . . . . . . 12 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → (∃𝑧𝐽 (𝐴𝑧 ∧ (𝐹𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g𝐺)𝐴))(+g𝐻)𝑤) ∈ 𝑦}) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
15560, 154mpd 15 . . . . . . . . . . 11 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥𝑋 ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦))) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
156155anassrs 467 . . . . . . . . . 10 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) ∧ (𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦)) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
157156expr 456 . . . . . . . . 9 (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) ∧ 𝑦𝐾) → ((𝐹𝑥) ∈ 𝑦 → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
158157ralrimiva 3146 . . . . . . . 8 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → ∀𝑦𝐾 ((𝐹𝑥) ∈ 𝑦 → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))
1598adantr 480 . . . . . . . . 9 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝐽 ∈ (TopOn‘𝑋))
16013adantr 480 . . . . . . . . 9 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
161 simpr 484 . . . . . . . . 9 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝑥𝑋)
162 iscnp 23245 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝑥𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑦𝐾 ((𝐹𝑥) ∈ 𝑦 → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))))
163159, 160, 161, 162syl3anc 1373 . . . . . . . 8 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑦𝐾 ((𝐹𝑥) ∈ 𝑦 → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦)))))
16417, 158, 163mpbir2and 713 . . . . . . 7 ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥𝑋) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
165164ralrimiva 3146 . . . . . 6 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
166 cncnp 23288 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
1678, 13, 166syl2anc 584 . . . . . 6 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
16816, 165, 167mpbir2and 713 . . . . 5 (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹 ∈ (𝐽 Cn 𝐾))
169168ex 412 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐹 ∈ (𝐽 Cn 𝐾)))
1703, 169jcad 512 . . 3 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝐴 𝐽𝐹 ∈ (𝐽 Cn 𝐾))))
1711cncnpi 23286 . . . 4 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 𝐽) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
172171ancoms 458 . . 3 ((𝐴 𝐽𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
173170, 172impbid1 225 . 2 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐴 𝐽𝐹 ∈ (𝐽 Cn 𝐾))))
1747, 28syl 17 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → 𝑋 = 𝐽)
175174eleq2d 2827 . . 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 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  {crab 3436  wss 3951   cuni 4907  cmpt 5225  ccnv 5684  dom cdm 5685  cima 5688  Fun wfun 6555   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  Basecbs 17247  +gcplusg 17297  TopOpenctopn 17466  0gc0g 17484  Grpcgrp 18951  invgcminusg 18952  -gcsg 18953   GrpHom cghm 19230  TopOnctopon 22916   Cn ccn 23232   CnP ccnp 23233  TopMndctmd 24078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-map 8868  df-0g 17486  df-topgen 17488  df-plusf 18652  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954  df-minusg 18955  df-sbg 18956  df-ghm 19231  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cn 23235  df-cnp 23236  df-tx 23570  df-tmd 24080
This theorem is referenced by:  qqhcn  33992
  Copyright terms: Public domain W3C validator