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 | |
|
Assertion | subgntr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subgntr.h | |
|
2 | df-ima | |
|
3 | eqid | |
|
4 | 1 3 | tgptopon | |
5 | 4 | 3ad2ant1 | |
6 | 5 | adantr | |
7 | topontop | |
|
8 | 5 7 | syl | |
9 | 8 | adantr | |
10 | simpl2 | |
|
11 | 3 | subgss | |
12 | 10 11 | syl | |
13 | toponuni | |
|
14 | 6 13 | syl | |
15 | 12 14 | sseqtrd | |
16 | eqid | |
|
17 | 16 | ntropn | |
18 | 9 15 17 | syl2anc | |
19 | toponss | |
|
20 | 6 18 19 | syl2anc | |
21 | 20 | resmptd | |
22 | 21 | rneqd | |
23 | 2 22 | eqtrid | |
24 | simpl1 | |
|
25 | simpr | |
|
26 | 16 | ntrss2 | |
27 | 9 15 26 | syl2anc | |
28 | simpl3 | |
|
29 | 27 28 | sseldd | |
30 | eqid | |
|
31 | 30 | subgsubcl | |
32 | 10 25 29 31 | syl3anc | |
33 | 12 32 | sseldd | |
34 | eqid | |
|
35 | eqid | |
|
36 | 34 3 35 1 | tgplacthmeo | |
37 | 24 33 36 | syl2anc | |
38 | hmeoima | |
|
39 | 37 18 38 | syl2anc | |
40 | 23 39 | eqeltrrd | |
41 | tgpgrp | |
|
42 | 24 41 | syl | |
43 | 11 | 3ad2ant2 | |
44 | 43 | sselda | |
45 | 20 28 | sseldd | |
46 | 3 35 30 | grpnpcan | |
47 | 42 44 45 46 | syl3anc | |
48 | ovex | |
|
49 | eqid | |
|
50 | oveq2 | |
|
51 | 49 50 | elrnmpt1s | |
52 | 28 48 51 | sylancl | |
53 | 47 52 | eqeltrrd | |
54 | 10 | adantr | |
55 | 32 | adantr | |
56 | 27 | sselda | |
57 | 35 | subgcl | |
58 | 54 55 56 57 | syl3anc | |
59 | 58 | fmpttd | |
60 | 59 | frnd | |
61 | eleq2 | |
|
62 | sseq1 | |
|
63 | 61 62 | anbi12d | |
64 | 63 | rspcev | |
65 | 40 53 60 64 | syl12anc | |
66 | 65 | ralrimiva | |
67 | eltop2 | |
|
68 | 8 67 | syl | |
69 | 66 68 | mpbird | |