tgpconncomp

Description: The identity component, the connected component containing the identity element, is a closed ( conncompcld ) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)

	Ref	Expression
Hypotheses	tgpconncomp.x	$⊢ X = {Base}_{G}$
	tgpconncomp.z	$⊢ \underset{˙}{0} = 0_{G}$
	tgpconncomp.j	$⊢ J = TopOpen (G)$
	tgpconncomp.s	$⊢ S = ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\}$
Assertion	tgpconncomp	$⊢ G \in TopGrp \to S \in NrmSGrp (G)$

Proof

Step	Hyp	Ref	Expression
1		tgpconncomp.x	$⊢ X = {Base}_{G}$
2		tgpconncomp.z	$⊢ \underset{˙}{0} = 0_{G}$
3		tgpconncomp.j	$⊢ J = TopOpen (G)$
4		tgpconncomp.s	$⊢ S = ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\}$
5		ssrab2	$⊢ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq 𝒫 X$
6		sspwuni	$⊢ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq 𝒫 X \leftrightarrow ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq X$
7	5 6	mpbi	$⊢ ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq X$
8	4 7	eqsstri	$⊢ S \subseteq X$
9	8	a1i	$⊢ G \in TopGrp \to S \subseteq X$
10	3 1	tgptopon	$⊢ G \in TopGrp \to J \in TopOn (X)$
11		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
12	1 2	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in X$
13	11 12	syl	$⊢ G \in TopGrp \to \underset{˙}{0} \in X$
14	4	conncompid	$⊢ (J \in TopOn (X) \land \underset{˙}{0} \in X) \to \underset{˙}{0} \in S$
15	10 13 14	syl2anc	$⊢ G \in TopGrp \to \underset{˙}{0} \in S$
16	15	ne0d	$⊢ G \in TopGrp \to S \neq \emptyset$
17		df-ima	$⊢ (z \in X ⟼ y -_{G} z) [S] = ran ({(z \in X ⟼ y -_{G} z) ↾}_{S})$
18		resmpt	$⊢ S \subseteq X \to {(z \in X ⟼ y -_{G} z) ↾}_{S} = (z \in S ⟼ y -_{G} z)$
19	8 18	ax-mp	$⊢ {(z \in X ⟼ y -_{G} z) ↾}_{S} = (z \in S ⟼ y -_{G} z)$
20	19	rneqi	$⊢ ran ({(z \in X ⟼ y -_{G} z) ↾}_{S}) = ran (z \in S ⟼ y -_{G} z)$
21	17 20	eqtri	$⊢ (z \in X ⟼ y -_{G} z) [S] = ran (z \in S ⟼ y -_{G} z)$
22		imassrn	$⊢ (z \in X ⟼ y -_{G} z) [S] \subseteq ran (z \in X ⟼ y -_{G} z)$
23	11	adantr	$⊢ (G \in TopGrp \land y \in S) \to G \in Grp$
24	23	adantr	$⊢ ((G \in TopGrp \land y \in S) \land z \in X) \to G \in Grp$
25	9	sselda	$⊢ (G \in TopGrp \land y \in S) \to y \in X$
26	25	adantr	$⊢ ((G \in TopGrp \land y \in S) \land z \in X) \to y \in X$
27		simpr	$⊢ ((G \in TopGrp \land y \in S) \land z \in X) \to z \in X$
28		eqid	$⊢ -_{G} = -_{G}$
29	1 28	grpsubcl	$⊢ (G \in Grp \land y \in X \land z \in X) \to y -_{G} z \in X$
30	24 26 27 29	syl3anc	$⊢ ((G \in TopGrp \land y \in S) \land z \in X) \to y -_{G} z \in X$
31	30	fmpttd	$⊢ (G \in TopGrp \land y \in S) \to (z \in X ⟼ y -_{G} z) : X ⟶ X$
32	31	frnd	$⊢ (G \in TopGrp \land y \in S) \to ran (z \in X ⟼ y -_{G} z) \subseteq X$
33	22 32	sstrid	$⊢ (G \in TopGrp \land y \in S) \to (z \in X ⟼ y -_{G} z) [S] \subseteq X$
34	1 2 28	grpsubid	$⊢ (G \in Grp \land y \in X) \to y -_{G} y = \underset{˙}{0}$
35	23 25 34	syl2anc	$⊢ (G \in TopGrp \land y \in S) \to y -_{G} y = \underset{˙}{0}$
36		simpr	$⊢ (G \in TopGrp \land y \in S) \to y \in S$
37		ovex	$⊢ y -_{G} y \in V$
38		eqid	$⊢ (z \in S ⟼ y -_{G} z) = (z \in S ⟼ y -_{G} z)$
39		oveq2	$⊢ z = y \to y -_{G} z = y -_{G} y$
40	38 39	elrnmpt1s	$⊢ (y \in S \land y -_{G} y \in V) \to y -_{G} y \in ran (z \in S ⟼ y -_{G} z)$
41	36 37 40	sylancl	$⊢ (G \in TopGrp \land y \in S) \to y -_{G} y \in ran (z \in S ⟼ y -_{G} z)$
42	35 41	eqeltrrd	$⊢ (G \in TopGrp \land y \in S) \to \underset{˙}{0} \in ran (z \in S ⟼ y -_{G} z)$
43	42 21	eleqtrrdi	$⊢ (G \in TopGrp \land y \in S) \to \underset{˙}{0} \in (z \in X ⟼ y -_{G} z) [S]$
44		eqid	$⊢ ⋃ J = ⋃ J$
45		eqid	$⊢ +_{G} = +_{G}$
46		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
47	1 45 46 28	grpsubval	$⊢ (y \in X \land z \in X) \to y -_{G} z = y +_{G} {inv}_{g} (G) (z)$
48	25 47	sylan	$⊢ ((G \in TopGrp \land y \in S) \land z \in X) \to y -_{G} z = y +_{G} {inv}_{g} (G) (z)$
49	48	mpteq2dva	$⊢ (G \in TopGrp \land y \in S) \to (z \in X ⟼ y -_{G} z) = (z \in X ⟼ y +_{G} {inv}_{g} (G) (z))$
50	1 46	grpinvcl	$⊢ (G \in Grp \land z \in X) \to {inv}_{g} (G) (z) \in X$
51	23 50	sylan	$⊢ ((G \in TopGrp \land y \in S) \land z \in X) \to {inv}_{g} (G) (z) \in X$
52	1 46	grpinvf	$⊢ G \in Grp \to {inv}_{g} (G) : X ⟶ X$
53	11 52	syl	$⊢ G \in TopGrp \to {inv}_{g} (G) : X ⟶ X$
54	53	adantr	$⊢ (G \in TopGrp \land y \in S) \to {inv}_{g} (G) : X ⟶ X$
55	54	feqmptd	$⊢ (G \in TopGrp \land y \in S) \to {inv}_{g} (G) = (z \in X ⟼ {inv}_{g} (G) (z))$
56		eqidd	$⊢ (G \in TopGrp \land y \in S) \to (w \in X ⟼ y +_{G} w) = (w \in X ⟼ y +_{G} w)$
57		oveq2	$⊢ w = {inv}_{g} (G) (z) \to y +_{G} w = y +_{G} {inv}_{g} (G) (z)$
58	51 55 56 57	fmptco	$⊢ (G \in TopGrp \land y \in S) \to (w \in X ⟼ y +_{G} w) \circ {inv}_{g} (G) = (z \in X ⟼ y +_{G} {inv}_{g} (G) (z))$
59	49 58	eqtr4d	$⊢ (G \in TopGrp \land y \in S) \to (z \in X ⟼ y -_{G} z) = (w \in X ⟼ y +_{G} w) \circ {inv}_{g} (G)$
60	3 46	grpinvhmeo	$⊢ G \in TopGrp \to {inv}_{g} (G) \in (J Homeo J)$
61	60	adantr	$⊢ (G \in TopGrp \land y \in S) \to {inv}_{g} (G) \in (J Homeo J)$
62		eqid	$⊢ (w \in X ⟼ y +_{G} w) = (w \in X ⟼ y +_{G} w)$
63	62 1 45 3	tgplacthmeo	$⊢ (G \in TopGrp \land y \in X) \to (w \in X ⟼ y +_{G} w) \in (J Homeo J)$
64	25 63	syldan	$⊢ (G \in TopGrp \land y \in S) \to (w \in X ⟼ y +_{G} w) \in (J Homeo J)$
65		hmeoco	$⊢ ({inv}_{g} (G) \in (J Homeo J) \land (w \in X ⟼ y +_{G} w) \in (J Homeo J)) \to (w \in X ⟼ y +_{G} w) \circ {inv}_{g} (G) \in (J Homeo J)$
66	61 64 65	syl2anc	$⊢ (G \in TopGrp \land y \in S) \to (w \in X ⟼ y +_{G} w) \circ {inv}_{g} (G) \in (J Homeo J)$
67	59 66	eqeltrd	$⊢ (G \in TopGrp \land y \in S) \to (z \in X ⟼ y -_{G} z) \in (J Homeo J)$
68		hmeocn	$⊢ (z \in X ⟼ y -_{G} z) \in (J Homeo J) \to (z \in X ⟼ y -_{G} z) \in (J Cn J)$
69	67 68	syl	$⊢ (G \in TopGrp \land y \in S) \to (z \in X ⟼ y -_{G} z) \in (J Cn J)$
70		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
71	10 70	syl	$⊢ G \in TopGrp \to X = ⋃ J$
72	71	adantr	$⊢ (G \in TopGrp \land y \in S) \to X = ⋃ J$
73	8 72	sseqtrid	$⊢ (G \in TopGrp \land y \in S) \to S \subseteq ⋃ J$
74	4	conncompconn	$⊢ (J \in TopOn (X) \land \underset{˙}{0} \in X) \to J ↾_{𝑡} S \in Conn$
75	10 13 74	syl2anc	$⊢ G \in TopGrp \to J ↾_{𝑡} S \in Conn$
76	75	adantr	$⊢ (G \in TopGrp \land y \in S) \to J ↾_{𝑡} S \in Conn$
77	44 69 73 76	connima	$⊢ (G \in TopGrp \land y \in S) \to J ↾_{𝑡} (z \in X ⟼ y -_{G} z) [S] \in Conn$
78	4	conncompss	$⊢ ((z \in X ⟼ y -_{G} z) [S] \subseteq X \land \underset{˙}{0} \in (z \in X ⟼ y -_{G} z) [S] \land J ↾_{𝑡} (z \in X ⟼ y -_{G} z) [S] \in Conn) \to (z \in X ⟼ y -_{G} z) [S] \subseteq S$
79	33 43 77 78	syl3anc	$⊢ (G \in TopGrp \land y \in S) \to (z \in X ⟼ y -_{G} z) [S] \subseteq S$
80	21 79	eqsstrrid	$⊢ (G \in TopGrp \land y \in S) \to ran (z \in S ⟼ y -_{G} z) \subseteq S$
81		ovex	$⊢ y -_{G} z \in V$
82	81 38	fnmpti	$⊢ (z \in S ⟼ y -_{G} z) Fn S$
83		df-f	$⊢ (z \in S ⟼ y -_{G} z) : S ⟶ S \leftrightarrow ((z \in S ⟼ y -_{G} z) Fn S \land ran (z \in S ⟼ y -_{G} z) \subseteq S)$
84	82 83	mpbiran	$⊢ (z \in S ⟼ y -_{G} z) : S ⟶ S \leftrightarrow ran (z \in S ⟼ y -_{G} z) \subseteq S$
85	80 84	sylibr	$⊢ (G \in TopGrp \land y \in S) \to (z \in S ⟼ y -_{G} z) : S ⟶ S$
86	38	fmpt	$⊢ \forall z \in S y -_{G} z \in S \leftrightarrow (z \in S ⟼ y -_{G} z) : S ⟶ S$
87	85 86	sylibr	$⊢ (G \in TopGrp \land y \in S) \to \forall z \in S y -_{G} z \in S$
88	87	ralrimiva	$⊢ G \in TopGrp \to \forall y \in S \forall z \in S y -_{G} z \in S$
89	1 28	issubg4	$⊢ G \in Grp \to (S \in SubGrp (G) \leftrightarrow (S \subseteq X \land S \neq \emptyset \land \forall y \in S \forall z \in S y -_{G} z \in S))$
90	11 89	syl	$⊢ G \in TopGrp \to (S \in SubGrp (G) \leftrightarrow (S \subseteq X \land S \neq \emptyset \land \forall y \in S \forall z \in S y -_{G} z \in S))$
91	9 16 88 90	mpbir3and	$⊢ G \in TopGrp \to S \in SubGrp (G)$
92	11	adantr	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to G \in Grp$
93		eqid	$⊢ {opp}_{𝑔} (G) = {opp}_{𝑔} (G)$
94	93 46	oppginv	$⊢ G \in Grp \to {inv}_{g} (G) = {inv}_{g} ({opp}_{𝑔} (G))$
95	92 94	syl	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} (G) = {inv}_{g} ({opp}_{𝑔} (G))$
96	95	fveq1d	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} (G) ({inv}_{g} (G) (y)) = {inv}_{g} ({opp}_{𝑔} (G)) ({inv}_{g} (G) (y))$
97		simprll	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to y \in X$
98	1 46	grpinvinv	$⊢ (G \in Grp \land y \in X) \to {inv}_{g} (G) ({inv}_{g} (G) (y)) = y$
99	92 97 98	syl2anc	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} (G) ({inv}_{g} (G) (y)) = y$
100	96 99	eqtr3d	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} ({opp}_{𝑔} (G)) ({inv}_{g} (G) (y)) = y$
101	100	oveq1d	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} ({opp}_{𝑔} (G)) ({inv}_{g} (G) (y)) +_{{opp}_{𝑔} (G)} z = y +_{{opp}_{𝑔} (G)} z$
102		eqid	$⊢ +_{{opp}_{𝑔} (G)} = +_{{opp}_{𝑔} (G)}$
103	45 93 102	oppgplus	$⊢ y +_{{opp}_{𝑔} (G)} z = z +_{G} y$
104	101 103	eqtrdi	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} ({opp}_{𝑔} (G)) ({inv}_{g} (G) (y)) +_{{opp}_{𝑔} (G)} z = z +_{G} y$
105	1 46	grpinvcl	$⊢ (G \in Grp \land y \in X) \to {inv}_{g} (G) (y) \in X$
106	92 97 105	syl2anc	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} (G) (y) \in X$
107		simprlr	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to z \in X$
108	99	oveq1d	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} (G) ({inv}_{g} (G) (y)) +_{G} z = y +_{G} z$
109		simprr	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to y +_{G} z \in S$
110	108 109	eqeltrd	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} (G) ({inv}_{g} (G) (y)) +_{G} z \in S$
111		eqid	$⊢ G ~_{QG} S = G ~_{QG} S$
112	1 46 45 111	eqgval	$⊢ (G \in Grp \land S \subseteq X) \to ({inv}_{g} (G) (y) (G ~_{QG} S) z \leftrightarrow ({inv}_{g} (G) (y) \in X \land z \in X \land {inv}_{g} (G) ({inv}_{g} (G) (y)) +_{G} z \in S))$
113	92 8 112	sylancl	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to ({inv}_{g} (G) (y) (G ~_{QG} S) z \leftrightarrow ({inv}_{g} (G) (y) \in X \land z \in X \land {inv}_{g} (G) ({inv}_{g} (G) (y)) +_{G} z \in S))$
114	106 107 110 113	mpbir3and	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} (G) (y) (G ~_{QG} S) z$
115	1 2 3 4 111	tgpconncompeqg	$⊢ (G \in TopGrp \land {inv}_{g} (G) (y) \in X) \to [{inv}_{g} (G) (y)] (G ~_{QG} S) = ⋃ \{x \in 𝒫 X \| ({inv}_{g} (G) (y) \in x \land J ↾_{𝑡} x \in Conn)\}$
116	106 115	syldan	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to [{inv}_{g} (G) (y)] (G ~_{QG} S) = ⋃ \{x \in 𝒫 X \| ({inv}_{g} (G) (y) \in x \land J ↾_{𝑡} x \in Conn)\}$
117	93	oppgtgp	$⊢ G \in TopGrp \to {opp}_{𝑔} (G) \in TopGrp$
118	117	adantr	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {opp}_{𝑔} (G) \in TopGrp$
119	93 1	oppgbas	$⊢ X = {Base}_{{opp}_{𝑔} (G)}$
120	93 2	oppgid	$⊢ \underset{˙}{0} = 0_{{opp}_{𝑔} (G)}$
121	93 3	oppgtopn	$⊢ J = TopOpen ({opp}_{𝑔} (G))$
122		eqid	$⊢ {opp}_{𝑔} (G) ~_{QG} S = {opp}_{𝑔} (G) ~_{QG} S$
123	119 120 121 4 122	tgpconncompeqg	$⊢ ({opp}_{𝑔} (G) \in TopGrp \land {inv}_{g} (G) (y) \in X) \to [{inv}_{g} (G) (y)] ({opp}_{𝑔} (G) ~_{QG} S) = ⋃ \{x \in 𝒫 X \| ({inv}_{g} (G) (y) \in x \land J ↾_{𝑡} x \in Conn)\}$
124	118 106 123	syl2anc	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to [{inv}_{g} (G) (y)] ({opp}_{𝑔} (G) ~_{QG} S) = ⋃ \{x \in 𝒫 X \| ({inv}_{g} (G) (y) \in x \land J ↾_{𝑡} x \in Conn)\}$
125	116 124	eqtr4d	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to [{inv}_{g} (G) (y)] (G ~_{QG} S) = [{inv}_{g} (G) (y)] ({opp}_{𝑔} (G) ~_{QG} S)$
126	125	eleq2d	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to (z \in [{inv}_{g} (G) (y)] (G ~_{QG} S) \leftrightarrow z \in [{inv}_{g} (G) (y)] ({opp}_{𝑔} (G) ~_{QG} S))$
127		vex	$⊢ z \in V$
128		fvex	$⊢ {inv}_{g} (G) (y) \in V$
129	127 128	elec	$⊢ z \in [{inv}_{g} (G) (y)] (G ~_{QG} S) \leftrightarrow {inv}_{g} (G) (y) (G ~_{QG} S) z$
130	127 128	elec	$⊢ z \in [{inv}_{g} (G) (y)] ({opp}_{𝑔} (G) ~_{QG} S) \leftrightarrow {inv}_{g} (G) (y) ({opp}_{𝑔} (G) ~_{QG} S) z$
131	126 129 130	3bitr3g	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to ({inv}_{g} (G) (y) (G ~_{QG} S) z \leftrightarrow {inv}_{g} (G) (y) ({opp}_{𝑔} (G) ~_{QG} S) z)$
132	114 131	mpbid	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} (G) (y) ({opp}_{𝑔} (G) ~_{QG} S) z$
133		eqid	$⊢ {inv}_{g} ({opp}_{𝑔} (G)) = {inv}_{g} ({opp}_{𝑔} (G))$
134	119 133 102 122	eqgval	$⊢ ({opp}_{𝑔} (G) \in TopGrp \land S \subseteq X) \to ({inv}_{g} (G) (y) ({opp}_{𝑔} (G) ~_{QG} S) z \leftrightarrow ({inv}_{g} (G) (y) \in X \land z \in X \land {inv}_{g} ({opp}_{𝑔} (G)) ({inv}_{g} (G) (y)) +_{{opp}_{𝑔} (G)} z \in S))$
135	118 8 134	sylancl	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to ({inv}_{g} (G) (y) ({opp}_{𝑔} (G) ~_{QG} S) z \leftrightarrow ({inv}_{g} (G) (y) \in X \land z \in X \land {inv}_{g} ({opp}_{𝑔} (G)) ({inv}_{g} (G) (y)) +_{{opp}_{𝑔} (G)} z \in S))$
136	132 135	mpbid	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to ({inv}_{g} (G) (y) \in X \land z \in X \land {inv}_{g} ({opp}_{𝑔} (G)) ({inv}_{g} (G) (y)) +_{{opp}_{𝑔} (G)} z \in S)$
137	136	simp3d	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to {inv}_{g} ({opp}_{𝑔} (G)) ({inv}_{g} (G) (y)) +_{{opp}_{𝑔} (G)} z \in S$
138	104 137	eqeltrrd	$⊢ (G \in TopGrp \land ((y \in X \land z \in X) \land y +_{G} z \in S)) \to z +_{G} y \in S$
139	138	expr	$⊢ (G \in TopGrp \land (y \in X \land z \in X)) \to (y +_{G} z \in S \to z +_{G} y \in S)$
140	139	ralrimivva	$⊢ G \in TopGrp \to \forall y \in X \forall z \in X (y +_{G} z \in S \to z +_{G} y \in S)$
141	1 45	isnsg2	$⊢ S \in NrmSGrp (G) \leftrightarrow (S \in SubGrp (G) \land \forall y \in X \forall z \in X (y +_{G} z \in S \to z +_{G} y \in S))$
142	91 140 141	sylanbrc	$⊢ G \in TopGrp \to S \in NrmSGrp (G)$

Metamath Proof Explorer

Theorem tgpconncomp

Proof