Theorem ghmcnp 22127

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.

Step	Hyp	Ref	Expression
1		eqid 2805	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	cnprcl 21259	. . . . 5 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐴 ∈ ∪ 𝐽)
3	2	a1i 11	. . . 4 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐴 ∈ ∪ 𝐽))
4		ghmcnp.j	. . . . . . . . . 10 ⊢ 𝐽 = (TopOpen‘𝐺)
5		ghmcnp.x	. . . . . . . . . 10 ⊢ 𝑋 = (Base‘𝐺)
6	4, 5	tmdtopon 22094	. . . . . . . . 9 ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝑋))
7	6	3ad2ant1 1156	. . . . . . . 8 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → 𝐽 ∈ (TopOn‘𝑋))
8	7	adantr 468	. . . . . . 7 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
9		simpl2 1237	. . . . . . . 8 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐻 ∈ TopMnd)
10		ghmcnp.k	. . . . . . . . 9 ⊢ 𝐾 = (TopOpen‘𝐻)
11		eqid 2805	. . . . . . . . 9 ⊢ (Base‘𝐻) = (Base‘𝐻)
12	10, 11	tmdtopon 22094	. . . . . . . 8 ⊢ (𝐻 ∈ TopMnd → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
13	9, 12	syl 17	. . . . . . 7 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
14		simpr 473	. . . . . . 7 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
15		cnpf2 21264	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶(Base‘𝐻))
16	8, 13, 14, 15	syl3anc 1483	. . . . . 6 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋⟶(Base‘𝐻))
17	16	adantr 468	. . . . . . . 8 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥 ∈ 𝑋) → 𝐹:𝑋⟶(Base‘𝐻))
18	14	adantr 468	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
19		eqid 2805	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤)) = (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤))
20	19	mptpreima 5839	. . . . . . . . . . . . . 14 ⊢ (◡(𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤)) “ 𝑦) = {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦}
21	9	adantr 468	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝐻 ∈ TopMnd)
22	16	adantr 468	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝐹:𝑋⟶(Base‘𝐻))
23		simpll3 1266	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
24		ghmgrp1 17860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp)
25	23, 24	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝐺 ∈ Grp)
26		simprl 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝑥 ∈ 𝑋)
27	2	adantl 469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐴 ∈ ∪ 𝐽)
28		toponuni 20928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
29	8, 28	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝑋 = ∪ 𝐽)
30	27, 29	eleqtrrd 2887	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐴 ∈ 𝑋)
31	30	adantr 468	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝐴 ∈ 𝑋)
32		eqid 2805	. . . . . . . . . . . . . . . . . . 19 ⊢ (-g‘𝐺) = (-g‘𝐺)
33	5, 32	grpsubcl 17696	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑥(-g‘𝐺)𝐴) ∈ 𝑋)
34	25, 26, 31, 33	syl3anc 1483	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (𝑥(-g‘𝐺)𝐴) ∈ 𝑋)
35	22, 34	ffvelrnd 6579	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (𝐹‘(𝑥(-g‘𝐺)𝐴)) ∈ (Base‘𝐻))
36		eqid 2805	. . . . . . . . . . . . . . . . 17 ⊢ (+g‘𝐻) = (+g‘𝐻)
37	19, 11, 36, 10	tmdlactcn 22115	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻 ∈ TopMnd ∧ (𝐹‘(𝑥(-g‘𝐺)𝐴)) ∈ (Base‘𝐻)) → (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤)) ∈ (𝐾 Cn 𝐾))
38	21, 35, 37	syl2anc 575	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤)) ∈ (𝐾 Cn 𝐾))
39		simprrl 790	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝑦 ∈ 𝐾)
40		cnima 21279	. . . . . . . . . . . . . . 15 ⊢ (((𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤)) ∈ (𝐾 Cn 𝐾) ∧ 𝑦 ∈ 𝐾) → (◡(𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤)) “ 𝑦) ∈ 𝐾)
41	38, 39, 40	syl2anc 575	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (◡(𝑤 ∈ (Base‘𝐻) ↦ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤)) “ 𝑦) ∈ 𝐾)
42	20, 41	syl5eqelr 2889	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦} ∈ 𝐾)
43	22, 31	ffvelrnd 6579	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (𝐹‘𝐴) ∈ (Base‘𝐻))
44		eqid 2805	. . . . . . . . . . . . . . . . . . 19 ⊢ (-g‘𝐻) = (-g‘𝐻)
45	5, 32, 44	ghmsub 17866	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐹‘(𝑥(-g‘𝐺)𝐴)) = ((𝐹‘𝑥)(-g‘𝐻)(𝐹‘𝐴)))
46	23, 26, 31, 45	syl3anc 1483	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (𝐹‘(𝑥(-g‘𝐺)𝐴)) = ((𝐹‘𝑥)(-g‘𝐻)(𝐹‘𝐴)))
47	46	oveq1d 6886	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝐴)) = (((𝐹‘𝑥)(-g‘𝐻)(𝐹‘𝐴))(+g‘𝐻)(𝐹‘𝐴)))
48		ghmgrp2 17861	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp)
49	23, 48	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝐻 ∈ Grp)
50	22, 26	ffvelrnd 6579	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (𝐹‘𝑥) ∈ (Base‘𝐻))
51	11, 36, 44	grpnpcan 17708	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻 ∈ Grp ∧ (𝐹‘𝑥) ∈ (Base‘𝐻) ∧ (𝐹‘𝐴) ∈ (Base‘𝐻)) → (((𝐹‘𝑥)(-g‘𝐻)(𝐹‘𝐴))(+g‘𝐻)(𝐹‘𝐴)) = (𝐹‘𝑥))
52	49, 50, 43, 51	syl3anc 1483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (((𝐹‘𝑥)(-g‘𝐻)(𝐹‘𝐴))(+g‘𝐻)(𝐹‘𝐴)) = (𝐹‘𝑥))
53	47, 52	eqtrd 2839	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝐴)) = (𝐹‘𝑥))
54		simprrr 791	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (𝐹‘𝑥) ∈ 𝑦)
55	53, 54	eqeltrd 2884	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝐴)) ∈ 𝑦)
56		oveq2 6879	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝐹‘𝐴) → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) = ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝐴)))
57	56	eleq1d 2869	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐹‘𝐴) → (((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦 ↔ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝐴)) ∈ 𝑦))
58	57	elrab 3558	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝐴) ∈ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦} ↔ ((𝐹‘𝐴) ∈ (Base‘𝐻) ∧ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝐴)) ∈ 𝑦))
59	43, 55, 58	sylanbrc 574	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (𝐹‘𝐴) ∈ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦})
60		cnpimaex 21270	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦} ∈ 𝐾 ∧ (𝐹‘𝐴) ∈ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦}) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦}))
61	18, 42, 59, 60	syl3anc 1483	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦}))
62		ssrab 3874	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 “ 𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦} ↔ ((𝐹 “ 𝑧) ⊆ (Base‘𝐻) ∧ ∀𝑤 ∈ (𝐹 “ 𝑧)((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦))
63	62	simprbi 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 “ 𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦} → ∀𝑤 ∈ (𝐹 “ 𝑧)((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦)
64	22	adantr 468	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) → 𝐹:𝑋⟶(Base‘𝐻))
65	64	ffnd 6254	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) → 𝐹 Fn 𝑋)
66	8	adantr 468	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → 𝐽 ∈ (TopOn‘𝑋))
67		toponss 20941	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → 𝑧 ⊆ 𝑋)
68	66, 67	sylan 571	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) → 𝑧 ⊆ 𝑋)
69		oveq2 6879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = (𝐹‘𝑣) → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) = ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)))
70	69	eleq1d 2869	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = (𝐹‘𝑣) → (((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦 ↔ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))
71	70	ralima 6720	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑧 ⊆ 𝑋) → (∀𝑤 ∈ (𝐹 “ 𝑧)((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))
72	65, 68, 71	syl2anc 575	. . . . . . . . . . . . . . 15 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) → (∀𝑤 ∈ (𝐹 “ 𝑧)((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))
73	63, 72	syl5ib 235	. . . . . . . . . . . . . 14 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) → ((𝐹 “ 𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦} → ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))
74		eqid 2805	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝑋 ↦ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)) = (𝑤 ∈ 𝑋 ↦ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))
75	74	mptpreima 5839	. . . . . . . . . . . . . . . . 17 ⊢ (◡(𝑤 ∈ 𝑋 ↦ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)) “ 𝑧) = {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧}
76		simpl1 1235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐺 ∈ TopMnd)
77	76	ad2antrr 708	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → 𝐺 ∈ TopMnd)
78	25	adantr 468	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → 𝐺 ∈ Grp)
79	31	adantr 468	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → 𝐴 ∈ 𝑋)
80	26	adantr 468	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → 𝑥 ∈ 𝑋)
81	5, 32	grpsubcl 17696	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐴(-g‘𝐺)𝑥) ∈ 𝑋)
82	78, 79, 80, 81	syl3anc 1483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → (𝐴(-g‘𝐺)𝑥) ∈ 𝑋)
83		eqid 2805	. . . . . . . . . . . . . . . . . . . 20 ⊢ (+g‘𝐺) = (+g‘𝐺)
84	74, 5, 83, 4	tmdlactcn 22115	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ TopMnd ∧ (𝐴(-g‘𝐺)𝑥) ∈ 𝑋) → (𝑤 ∈ 𝑋 ↦ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)) ∈ (𝐽 Cn 𝐽))
85	77, 82, 84	syl2anc 575	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → (𝑤 ∈ 𝑋 ↦ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)) ∈ (𝐽 Cn 𝐽))
86		simprl 778	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → 𝑧 ∈ 𝐽)
87		cnima 21279	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 ∈ 𝑋 ↦ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)) ∈ (𝐽 Cn 𝐽) ∧ 𝑧 ∈ 𝐽) → (◡(𝑤 ∈ 𝑋 ↦ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)) “ 𝑧) ∈ 𝐽)
88	85, 86, 87	syl2anc 575	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → (◡(𝑤 ∈ 𝑋 ↦ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)) “ 𝑧) ∈ 𝐽)
89	75, 88	syl5eqelr 2889	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} ∈ 𝐽)
90	5, 83, 32	grpnpcan 17708	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑥) = 𝐴)
91	78, 79, 80, 90	syl3anc 1483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑥) = 𝐴)
92		simprrl 790	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → 𝐴 ∈ 𝑧)
93	91, 92	eqeltrd 2884	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑥) ∈ 𝑧)
94		oveq2 6879	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑥 → ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) = ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑥))
95	94	eleq1d 2869	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑥 → (((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧 ↔ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑥) ∈ 𝑧))
96	95	elrab 3558	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} ↔ (𝑥 ∈ 𝑋 ∧ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑥) ∈ 𝑧))
97	80, 93, 96	sylanbrc 574	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → 𝑥 ∈ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧})
98		simprrr 791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦)
99		fveq2 6405	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) → (𝐹‘𝑣) = (𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)))
100	99	oveq2d 6887	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) = ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))))
101	100	eleq1d 2869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) → (((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦 ↔ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) ∈ 𝑦))
102	101	rspccv 3498	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦 → (((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧 → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) ∈ 𝑦))
103	98, 102	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → (((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧 → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) ∈ 𝑦))
104	103	adantr 468	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → (((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧 → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) ∈ 𝑦))
105	23	adantr 468	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
106	34	adantr 468	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → (𝑥(-g‘𝐺)𝐴) ∈ 𝑋)
107	105, 24	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → 𝐺 ∈ Grp)
108	31	adantr 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → 𝐴 ∈ 𝑋)
109	26	adantr 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → 𝑥 ∈ 𝑋)
110	107, 108, 109, 81	syl3anc 1483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → (𝐴(-g‘𝐺)𝑥) ∈ 𝑋)
111		simpr 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑋)
112	5, 83	grpcl 17631	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺 ∈ Grp ∧ (𝐴(-g‘𝐺)𝑥) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑋)
113	107, 110, 111, 112	syl3anc 1483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑋)
114	5, 83, 36	ghmlin 17863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑥(-g‘𝐺)𝐴) ∈ 𝑋 ∧ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑋) → (𝐹‘((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) = ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))))
115	105, 106, 113, 114	syl3anc 1483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → (𝐹‘((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) = ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))))
116		eqid 2805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (invg‘𝐺) = (invg‘𝐺)
117	5, 32, 116	grpinvsub 17698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((invg‘𝐺)‘(𝑥(-g‘𝐺)𝐴)) = (𝐴(-g‘𝐺)𝑥))
118	107, 109, 108, 117	syl3anc 1483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → ((invg‘𝐺)‘(𝑥(-g‘𝐺)𝐴)) = (𝐴(-g‘𝐺)𝑥))
119	118	oveq2d 6887	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → ((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)((invg‘𝐺)‘(𝑥(-g‘𝐺)𝐴))) = ((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)(𝐴(-g‘𝐺)𝑥)))
120		eqid 2805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (0g‘𝐺) = (0g‘𝐺)
121	5, 83, 120, 116	grprinv 17670	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐺 ∈ Grp ∧ (𝑥(-g‘𝐺)𝐴) ∈ 𝑋) → ((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)((invg‘𝐺)‘(𝑥(-g‘𝐺)𝐴))) = (0g‘𝐺))
122	107, 106, 121	syl2anc 575	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → ((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)((invg‘𝐺)‘(𝑥(-g‘𝐺)𝐴))) = (0g‘𝐺))
123	119, 122	eqtr3d 2841	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → ((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)(𝐴(-g‘𝐺)𝑥)) = (0g‘𝐺))
124	123	oveq1d 6886	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → (((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)(𝐴(-g‘𝐺)𝑥))(+g‘𝐺)𝑤) = ((0g‘𝐺)(+g‘𝐺)𝑤))
125	5, 83	grpass 17632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺 ∈ Grp ∧ ((𝑥(-g‘𝐺)𝐴) ∈ 𝑋 ∧ (𝐴(-g‘𝐺)𝑥) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)(𝐴(-g‘𝐺)𝑥))(+g‘𝐺)𝑤) = ((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)))
126	107, 106, 110, 111, 125	syl13anc 1484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → (((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)(𝐴(-g‘𝐺)𝑥))(+g‘𝐺)𝑤) = ((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)))
127	5, 83, 120	grplid 17653	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋) → ((0g‘𝐺)(+g‘𝐺)𝑤) = 𝑤)
128	107, 111, 127	syl2anc 575	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → ((0g‘𝐺)(+g‘𝐺)𝑤) = 𝑤)
129	124, 126, 128	3eqtr3d 2847	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → ((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤)) = 𝑤)
130	129	fveq2d 6409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → (𝐹‘((𝑥(-g‘𝐺)𝐴)(+g‘𝐺)((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) = (𝐹‘𝑤))
131	115, 130	eqtr3d 2841	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) = (𝐹‘𝑤))
132	131	adantlr 697	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) = (𝐹‘𝑤))
133	132	eleq1d 2869	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → (((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤))) ∈ 𝑦 ↔ (𝐹‘𝑤) ∈ 𝑦))
134	104, 133	sylibd 230	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) ∧ 𝑤 ∈ 𝑋) → (((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧 → (𝐹‘𝑤) ∈ 𝑦))
135	134	ralrimiva 3153	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → ∀𝑤 ∈ 𝑋 (((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧 → (𝐹‘𝑤) ∈ 𝑦))
136		fveq2 6405	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = 𝑤 → (𝐹‘𝑣) = (𝐹‘𝑤))
137	136	eleq1d 2869	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → ((𝐹‘𝑣) ∈ 𝑦 ↔ (𝐹‘𝑤) ∈ 𝑦))
138	137	ralrab2 3567	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑣 ∈ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} (𝐹‘𝑣) ∈ 𝑦 ↔ ∀𝑤 ∈ 𝑋 (((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧 → (𝐹‘𝑤) ∈ 𝑦))
139	135, 138	sylibr 225	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → ∀𝑣 ∈ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} (𝐹‘𝑣) ∈ 𝑦)
140	22	adantr 468	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → 𝐹:𝑋⟶(Base‘𝐻))
141	140	ffund 6257	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → Fun 𝐹)
142		ssrab2 3881	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} ⊆ 𝑋
143	140	fdmd 6262	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → dom 𝐹 = 𝑋)
144	142, 143	syl5sseqr 3848	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} ⊆ dom 𝐹)
145		funimass4 6465	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐹 ∧ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} ⊆ dom 𝐹) → ((𝐹 “ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦 ↔ ∀𝑣 ∈ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} (𝐹‘𝑣) ∈ 𝑦))
146	141, 144, 145	syl2anc 575	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → ((𝐹 “ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦 ↔ ∀𝑣 ∈ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} (𝐹‘𝑣) ∈ 𝑦))
147	139, 146	mpbird 248	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → (𝐹 “ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦)
148		eleq2 2873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧}))
149		imaeq2 5669	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} → (𝐹 “ 𝑢) = (𝐹 “ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧}))
150	149	sseq1d 3826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} → ((𝐹 “ 𝑢) ⊆ 𝑦 ↔ (𝐹 “ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦))
151	148, 150	anbi12d 618	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} → ((𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦) ↔ (𝑥 ∈ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} ∧ (𝐹 “ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦)))
152	151	rspcev 3501	. . . . . . . . . . . . . . . 16 ⊢ (({𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} ∈ 𝐽 ∧ (𝑥 ∈ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧} ∧ (𝐹 “ {𝑤 ∈ 𝑋 ∣ ((𝐴(-g‘𝐺)𝑥)(+g‘𝐺)𝑤) ∈ 𝑧}) ⊆ 𝑦)) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦))
153	89, 97, 147, 152	syl12anc 856	. . . . . . . . . . . . . . 15 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ (𝑧 ∈ 𝐽 ∧ (𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦))) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦))
154	153	expr 446	. . . . . . . . . . . . . 14 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) → ((𝐴 ∈ 𝑧 ∧ ∀𝑣 ∈ 𝑧 ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)(𝐹‘𝑣)) ∈ 𝑦) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦)))
155	73, 154	sylan2d 594	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) ∧ 𝑧 ∈ 𝐽) → ((𝐴 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦}) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦)))
156	155	rexlimdva 3218	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → (∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ (𝐹 “ 𝑧) ⊆ {𝑤 ∈ (Base‘𝐻) ∣ ((𝐹‘(𝑥(-g‘𝐺)𝐴))(+g‘𝐻)𝑤) ∈ 𝑦}) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦)))
157	61, 156	mpd 15	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦))) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦))
158	157	anassrs 455	. . . . . . . . . 10 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦)) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦))
159	158	expr 446	. . . . . . . . 9 ⊢ (((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝐾) → ((𝐹‘𝑥) ∈ 𝑦 → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦)))
160	159	ralrimiva 3153	. . . . . . . 8 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝐾 ((𝐹‘𝑥) ∈ 𝑦 → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦)))
161	8	adantr 468	. . . . . . . . 9 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
162	13	adantr 468	. . . . . . . . 9 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘(Base‘𝐻)))
163		simpr 473	. . . . . . . . 9 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
164		iscnp 21251	. . . . . . . . 9 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻)) ∧ 𝑥 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑥) ∈ 𝑦 → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦)))))
165	161, 162, 163, 164	syl3anc 1483	. . . . . . . 8 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑥) ∈ 𝑦 → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦)))))
166	17, 160, 165	mpbir2and 695	. . . . . . 7 ⊢ ((((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ 𝑥 ∈ 𝑋) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
167	166	ralrimiva 3153	. . . . . 6 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
168		cncnp 21294	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘(Base‘𝐻))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
169	8, 13, 168	syl2anc 575	. . . . . 6 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶(Base‘𝐻) ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
170	16, 167, 169	mpbir2and 695	. . . . 5 ⊢ (((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹 ∈ (𝐽 Cn 𝐾))
171	170	ex 399	. . . 4 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐹 ∈ (𝐽 Cn 𝐾)))
172	3, 171	jcad 504	. . 3 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝐴 ∈ ∪ 𝐽 ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))
173	1	cncnpi 21292	. . . 4 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ ∪ 𝐽) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
174	173	ancoms 448	. . 3 ⊢ ((𝐴 ∈ ∪ 𝐽 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
175	172, 174	impbid1 216	. 2 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐴 ∈ ∪ 𝐽 ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))
176	7, 28	syl 17	. . . 4 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → 𝑋 = ∪ 𝐽)
177	176	eleq2d 2870	. . 3 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ∪ 𝐽))
178	177	anbi1d 617	. 2 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → ((𝐴 ∈ 𝑋 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ↔ (𝐴 ∈ ∪ 𝐽 ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))
179	175, 178	bitr4d 273	1 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐻 ∈ TopMnd ∧ 𝐹 ∈ (𝐺 GrpHom 𝐻)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐴 ∈ 𝑋 ∧ 𝐹 ∈ (𝐽 Cn 𝐾))))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∧ w3a 1100   = wceq 1637   ∈ wcel 2158  ∀wral 3095  ∃wrex 3096  {crab 3099   ⊆ wss 3766  ∪ cuni 4626   ↦ cmpt 4919  ^◡ccnv 5307  dom cdm 5308   “ cima 5311  Fun wfun 6092   Fn wfn 6093  ⟶wf 6094  ‘cfv 6098  (class class class)co 6871  Basecbs 16064  +_gcplusg 16149  TopOpenctopn 16283  0_gc0g 16301  Grpcgrp 17623  inv_gcminusg 17624  -_gcsg 17625   GrpHom cghm 17855  TopOnctopon 20924   Cn ccn 21238   CnP ccnp 21239  TopMndctmd 22083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4627  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-id 5216  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-1st 7395  df-2nd 7396  df-map 8091  df-0g 16303  df-topgen 16305  df-plusf 17442  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-grp 17626  df-minusg 17627  df-sbg 17628  df-ghm 17856  df-top 20908  df-topon 20925  df-topsp 20947  df-bases 20960  df-cn 21241  df-cnp 21242  df-tx 21575  df-tmd 22085

This theorem is referenced by:  qqhcn  30357