subgtgp

Description: A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015)

		Ref	Expression
	Hypothesis	subgtgp.h	$⊢ H = G ↾_{𝑠} S$
	Assertion	subgtgp	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to H \in TopGrp$

Proof

Step	Hyp	Ref	Expression
1		subgtgp.h	$⊢ H = G ↾_{𝑠} S$
2	1	subggrp	$⊢ S \in SubGrp (G) \to H \in Grp$
3	2	adantl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to H \in Grp$
4		tgptmd	$⊢ G \in TopGrp \to G \in TopMnd$
5		subgsubm	$⊢ S \in SubGrp (G) \to S \in SubMnd (G)$
6	1	submtmd	$⊢ (G \in TopMnd \land S \in SubMnd (G)) \to H \in TopMnd$
7	4 5 6	syl2an	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to H \in TopMnd$
8	1	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{H}$
9	8	adantl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to S = {Base}_{H}$
10	9	mpteq1d	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to (x \in S ⟼ {inv}_{g} (H) (x)) = (x \in {Base}_{H} ⟼ {inv}_{g} (H) (x))$
11		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
12		eqid	$⊢ {inv}_{g} (H) = {inv}_{g} (H)$
13	1 11 12	subginv	$⊢ (S \in SubGrp (G) \land x \in S) \to {inv}_{g} (G) (x) = {inv}_{g} (H) (x)$
14	13	adantll	$⊢ ((G \in TopGrp \land S \in SubGrp (G)) \land x \in S) \to {inv}_{g} (G) (x) = {inv}_{g} (H) (x)$
15	14	mpteq2dva	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to (x \in S ⟼ {inv}_{g} (G) (x)) = (x \in S ⟼ {inv}_{g} (H) (x))$
16		eqid	$⊢ {Base}_{H} = {Base}_{H}$
17	16 12	grpinvf	$⊢ H \in Grp \to {inv}_{g} (H) : {Base}_{H} ⟶ {Base}_{H}$
18	3 17	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {inv}_{g} (H) : {Base}_{H} ⟶ {Base}_{H}$
19	18	feqmptd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {inv}_{g} (H) = (x \in {Base}_{H} ⟼ {inv}_{g} (H) (x))$
20	10 15 19	3eqtr4rd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {inv}_{g} (H) = (x \in S ⟼ {inv}_{g} (G) (x))$
21		eqid	$⊢ TopOpen (G) ↾_{𝑡} S = TopOpen (G) ↾_{𝑡} S$
22		eqid	$⊢ TopOpen (G) = TopOpen (G)$
23		eqid	$⊢ {Base}_{G} = {Base}_{G}$
24	22 23	tgptopon	$⊢ G \in TopGrp \to TopOpen (G) \in TopOn ({Base}_{G})$
25	24	adantr	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to TopOpen (G) \in TopOn ({Base}_{G})$
26	23	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
27	26	adantl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to S \subseteq {Base}_{G}$
28		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
29	28	adantr	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to G \in Grp$
30	23 11	grpinvf	$⊢ G \in Grp \to {inv}_{g} (G) : {Base}_{G} ⟶ {Base}_{G}$
31	29 30	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {inv}_{g} (G) : {Base}_{G} ⟶ {Base}_{G}$
32	31	feqmptd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {inv}_{g} (G) = (x \in {Base}_{G} ⟼ {inv}_{g} (G) (x))$
33	22 11	tgpinv	$⊢ G \in TopGrp \to {inv}_{g} (G) \in (TopOpen (G) Cn TopOpen (G))$
34	33	adantr	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {inv}_{g} (G) \in (TopOpen (G) Cn TopOpen (G))$
35	32 34	eqeltrrd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to (x \in {Base}_{G} ⟼ {inv}_{g} (G) (x)) \in (TopOpen (G) Cn TopOpen (G))$
36	21 25 27 35	cnmpt1res	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to (x \in S ⟼ {inv}_{g} (G) (x)) \in ((TopOpen (G) ↾_{𝑡} S) Cn TopOpen (G))$
37	20 36	eqeltrd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {inv}_{g} (H) \in ((TopOpen (G) ↾_{𝑡} S) Cn TopOpen (G))$
38	18	frnd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to ran {inv}_{g} (H) \subseteq {Base}_{H}$
39	38 9	sseqtrrd	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to ran {inv}_{g} (H) \subseteq S$
40		cnrest2	$⊢ (TopOpen (G) \in TopOn ({Base}_{G}) \land ran {inv}_{g} (H) \subseteq S \land S \subseteq {Base}_{G}) \to ({inv}_{g} (H) \in ((TopOpen (G) ↾_{𝑡} S) Cn TopOpen (G)) \leftrightarrow {inv}_{g} (H) \in ((TopOpen (G) ↾_{𝑡} S) Cn (TopOpen (G) ↾_{𝑡} S)))$
41	25 39 27 40	syl3anc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to ({inv}_{g} (H) \in ((TopOpen (G) ↾_{𝑡} S) Cn TopOpen (G)) \leftrightarrow {inv}_{g} (H) \in ((TopOpen (G) ↾_{𝑡} S) Cn (TopOpen (G) ↾_{𝑡} S)))$
42	37 41	mpbid	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to {inv}_{g} (H) \in ((TopOpen (G) ↾_{𝑡} S) Cn (TopOpen (G) ↾_{𝑡} S))$
43	1 22	resstopn	$⊢ TopOpen (G) ↾_{𝑡} S = TopOpen (H)$
44	43 12	istgp	$⊢ H \in TopGrp \leftrightarrow (H \in Grp \land H \in TopMnd \land {inv}_{g} (H) \in ((TopOpen (G) ↾_{𝑡} S) Cn (TopOpen (G) ↾_{𝑡} S)))$
45	3 7 42 44	syl3anbrc	$⊢ (G \in TopGrp \land S \in SubGrp (G)) \to H \in TopGrp$

Metamath Proof Explorer

Theorem subgtgp

Proof