subgntr

Description: A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg , the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015)

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

Proof

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

Metamath Proof Explorer

Theorem subgntr

Proof