ghmcnp

Description: A group homomorphism on topological groups is continuous everywhere if it is continuous at any point. (Contributed by Mario Carneiro, 21-Oct-2015)

	Ref	Expression
Hypotheses	ghmcnp.x	$⊢ X = {Base}_{G}$
	ghmcnp.j	$⊢ J = TopOpen (G)$
	ghmcnp.k	$⊢ K = TopOpen (H)$
Assertion	ghmcnp	$⊢ (G \in TopMnd \land H \in TopMnd \land F \in (G GrpHom H)) \to (F \in (J CnP K) (A) \leftrightarrow (A \in X \land F \in (J Cn K)))$

Proof

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

Metamath Proof Explorer

Theorem ghmcnp

Proof