opnsubg

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

		Ref	Expression
	Hypothesis	subgntr.h	$⊢ J = TopOpen (G)$
	Assertion	opnsubg	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to S \in Clsd (J)$

Proof

Step	Hyp	Ref	Expression
1		subgntr.h	$⊢ J = TopOpen (G)$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3	2	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
4	3	3ad2ant2	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to S \subseteq {Base}_{G}$
5	1 2	tgptopon	$⊢ G \in TopGrp \to J \in TopOn ({Base}_{G})$
6	5	3ad2ant1	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to J \in TopOn ({Base}_{G})$
7		toponuni	$⊢ J \in TopOn ({Base}_{G}) \to {Base}_{G} = ⋃ J$
8	6 7	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to {Base}_{G} = ⋃ J$
9	4 8	sseqtrd	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to S \subseteq ⋃ J$
10	8	difeq1d	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to {Base}_{G} ∖ S = ⋃ J ∖ S$
11		df-ima	$⊢ (y \in {Base}_{G} ⟼ x +_{G} y) [S] = ran ({(y \in {Base}_{G} ⟼ x +_{G} y) ↾}_{S})$
12	4	adantr	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to S \subseteq {Base}_{G}$
13	12	resmptd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to {(y \in {Base}_{G} ⟼ x +_{G} y) ↾}_{S} = (y \in S ⟼ x +_{G} y)$
14	13	rneqd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to ran ({(y \in {Base}_{G} ⟼ x +_{G} y) ↾}_{S}) = ran (y \in S ⟼ x +_{G} y)$
15	11 14	syl5eq	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to (y \in {Base}_{G} ⟼ x +_{G} y) [S] = ran (y \in S ⟼ x +_{G} y)$
16		simpl1	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to G \in TopGrp$
17		eldifi	$⊢ x \in ({Base}_{G} ∖ S) \to x \in {Base}_{G}$
18	17	adantl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to x \in {Base}_{G}$
19		eqid	$⊢ (y \in {Base}_{G} ⟼ x +_{G} y) = (y \in {Base}_{G} ⟼ x +_{G} y)$
20		eqid	$⊢ +_{G} = +_{G}$
21	19 2 20 1	tgplacthmeo	$⊢ (G \in TopGrp \land x \in {Base}_{G}) \to (y \in {Base}_{G} ⟼ x +_{G} y) \in (J Homeo J)$
22	16 18 21	syl2anc	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to (y \in {Base}_{G} ⟼ x +_{G} y) \in (J Homeo J)$
23		simpl3	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to S \in J$
24		hmeoima	$⊢ ((y \in {Base}_{G} ⟼ x +_{G} y) \in (J Homeo J) \land S \in J) \to (y \in {Base}_{G} ⟼ x +_{G} y) [S] \in J$
25	22 23 24	syl2anc	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to (y \in {Base}_{G} ⟼ x +_{G} y) [S] \in J$
26	15 25	eqeltrrd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to ran (y \in S ⟼ x +_{G} y) \in J$
27		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
28	16 27	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to G \in Grp$
29		eqid	$⊢ 0_{G} = 0_{G}$
30	2 20 29	grprid	$⊢ (G \in Grp \land x \in {Base}_{G}) \to x +_{G} 0_{G} = x$
31	28 18 30	syl2anc	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to x +_{G} 0_{G} = x$
32		simpl2	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to S \in SubGrp (G)$
33	29	subg0cl	$⊢ S \in SubGrp (G) \to 0_{G} \in S$
34	32 33	syl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to 0_{G} \in S$
35		ovex	$⊢ x +_{G} 0_{G} \in V$
36		eqid	$⊢ (y \in S ⟼ x +_{G} y) = (y \in S ⟼ x +_{G} y)$
37		oveq2	$⊢ y = 0_{G} \to x +_{G} y = x +_{G} 0_{G}$
38	36 37	elrnmpt1s	$⊢ (0_{G} \in S \land x +_{G} 0_{G} \in V) \to x +_{G} 0_{G} \in ran (y \in S ⟼ x +_{G} y)$
39	34 35 38	sylancl	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to x +_{G} 0_{G} \in ran (y \in S ⟼ x +_{G} y)$
40	31 39	eqeltrrd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to x \in ran (y \in S ⟼ x +_{G} y)$
41	28	adantr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to G \in Grp$
42	18	adantr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to x \in {Base}_{G}$
43	12	sselda	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to y \in {Base}_{G}$
44	2 20	grpcl	$⊢ (G \in Grp \land x \in {Base}_{G} \land y \in {Base}_{G}) \to x +_{G} y \in {Base}_{G}$
45	41 42 43 44	syl3anc	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to x +_{G} y \in {Base}_{G}$
46		eldifn	$⊢ x \in ({Base}_{G} ∖ S) \to \neg x \in S$
47	46	ad2antlr	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to \neg x \in S$
48		eqid	$⊢ -_{G} = -_{G}$
49	48	subgsubcl	$⊢ (S \in SubGrp (G) \land x +_{G} y \in S \land y \in S) \to (x +_{G} y) -_{G} y \in S$
50	49	3com23	$⊢ (S \in SubGrp (G) \land y \in S \land x +_{G} y \in S) \to (x +_{G} y) -_{G} y \in S$
51	50	3expia	$⊢ (S \in SubGrp (G) \land y \in S) \to (x +_{G} y \in S \to (x +_{G} y) -_{G} y \in S)$
52	32 51	sylan	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to (x +_{G} y \in S \to (x +_{G} y) -_{G} y \in S)$
53	2 20 48	grppncan	$⊢ (G \in Grp \land x \in {Base}_{G} \land y \in {Base}_{G}) \to (x +_{G} y) -_{G} y = x$
54	41 42 43 53	syl3anc	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to (x +_{G} y) -_{G} y = x$
55	54	eleq1d	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to ((x +_{G} y) -_{G} y \in S \leftrightarrow x \in S)$
56	52 55	sylibd	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to (x +_{G} y \in S \to x \in S)$
57	47 56	mtod	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to \neg x +_{G} y \in S$
58	45 57	eldifd	$⊢ (((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \land y \in S) \to x +_{G} y \in ({Base}_{G} ∖ S)$
59	58	fmpttd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to (y \in S ⟼ x +_{G} y) : S ⟶ {Base}_{G} ∖ S$
60	59	frnd	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to ran (y \in S ⟼ x +_{G} y) \subseteq {Base}_{G} ∖ S$
61		eleq2	$⊢ u = ran (y \in S ⟼ x +_{G} y) \to (x \in u \leftrightarrow x \in ran (y \in S ⟼ x +_{G} y))$
62		sseq1	$⊢ u = ran (y \in S ⟼ x +_{G} y) \to (u \subseteq {Base}_{G} ∖ S \leftrightarrow ran (y \in S ⟼ x +_{G} y) \subseteq {Base}_{G} ∖ S)$
63	61 62	anbi12d	$⊢ u = ran (y \in S ⟼ x +_{G} y) \to ((x \in u \land u \subseteq {Base}_{G} ∖ S) \leftrightarrow (x \in ran (y \in S ⟼ x +_{G} y) \land ran (y \in S ⟼ x +_{G} y) \subseteq {Base}_{G} ∖ S))$
64	63	rspcev	$⊢ (ran (y \in S ⟼ x +_{G} y) \in J \land (x \in ran (y \in S ⟼ x +_{G} y) \land ran (y \in S ⟼ x +_{G} y) \subseteq {Base}_{G} ∖ S)) \to \exists u \in J (x \in u \land u \subseteq {Base}_{G} ∖ S)$
65	26 40 60 64	syl12anc	$⊢ ((G \in TopGrp \land S \in SubGrp (G) \land S \in J) \land x \in ({Base}_{G} ∖ S)) \to \exists u \in J (x \in u \land u \subseteq {Base}_{G} ∖ S)$
66	65	ralrimiva	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to \forall x \in ({Base}_{G} ∖ S) \exists u \in J (x \in u \land u \subseteq {Base}_{G} ∖ S)$
67		topontop	$⊢ J \in TopOn ({Base}_{G}) \to J \in Top$
68	6 67	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to J \in Top$
69		eltop2	$⊢ J \in Top \to ({Base}_{G} ∖ S \in J \leftrightarrow \forall x \in ({Base}_{G} ∖ S) \exists u \in J (x \in u \land u \subseteq {Base}_{G} ∖ S))$
70	68 69	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to ({Base}_{G} ∖ S \in J \leftrightarrow \forall x \in ({Base}_{G} ∖ S) \exists u \in J (x \in u \land u \subseteq {Base}_{G} ∖ S))$
71	66 70	mpbird	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to {Base}_{G} ∖ S \in J$
72	10 71	eqeltrrd	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to ⋃ J ∖ S \in J$
73		eqid	$⊢ ⋃ J = ⋃ J$
74	73	iscld	$⊢ J \in Top \to (S \in Clsd (J) \leftrightarrow (S \subseteq ⋃ J \land ⋃ J ∖ S \in J))$
75	68 74	syl	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to (S \in Clsd (J) \leftrightarrow (S \subseteq ⋃ J \land ⋃ J ∖ S \in J))$
76	9 72 75	mpbir2and	$⊢ (G \in TopGrp \land S \in SubGrp (G) \land S \in J) \to S \in Clsd (J)$

Metamath Proof Explorer

Theorem opnsubg

Proof