Metamath Proof Explorer


Theorem 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=TopOpenG
Assertion subgntr GTopGrpSSubGrpGAintJSSJ

Proof

Step Hyp Ref Expression
1 subgntr.h J=TopOpenG
2 df-ima yBaseGx-GA+GyintJS=ranyBaseGx-GA+GyintJS
3 eqid BaseG=BaseG
4 1 3 tgptopon GTopGrpJTopOnBaseG
5 4 3ad2ant1 GTopGrpSSubGrpGAintJSJTopOnBaseG
6 5 adantr GTopGrpSSubGrpGAintJSxSJTopOnBaseG
7 topontop JTopOnBaseGJTop
8 5 7 syl GTopGrpSSubGrpGAintJSJTop
9 8 adantr GTopGrpSSubGrpGAintJSxSJTop
10 simpl2 GTopGrpSSubGrpGAintJSxSSSubGrpG
11 3 subgss SSubGrpGSBaseG
12 10 11 syl GTopGrpSSubGrpGAintJSxSSBaseG
13 toponuni JTopOnBaseGBaseG=J
14 6 13 syl GTopGrpSSubGrpGAintJSxSBaseG=J
15 12 14 sseqtrd GTopGrpSSubGrpGAintJSxSSJ
16 eqid J=J
17 16 ntropn JTopSJintJSJ
18 9 15 17 syl2anc GTopGrpSSubGrpGAintJSxSintJSJ
19 toponss JTopOnBaseGintJSJintJSBaseG
20 6 18 19 syl2anc GTopGrpSSubGrpGAintJSxSintJSBaseG
21 20 resmptd GTopGrpSSubGrpGAintJSxSyBaseGx-GA+GyintJS=yintJSx-GA+Gy
22 21 rneqd GTopGrpSSubGrpGAintJSxSranyBaseGx-GA+GyintJS=ranyintJSx-GA+Gy
23 2 22 eqtrid GTopGrpSSubGrpGAintJSxSyBaseGx-GA+GyintJS=ranyintJSx-GA+Gy
24 simpl1 GTopGrpSSubGrpGAintJSxSGTopGrp
25 simpr GTopGrpSSubGrpGAintJSxSxS
26 16 ntrss2 JTopSJintJSS
27 9 15 26 syl2anc GTopGrpSSubGrpGAintJSxSintJSS
28 simpl3 GTopGrpSSubGrpGAintJSxSAintJS
29 27 28 sseldd GTopGrpSSubGrpGAintJSxSAS
30 eqid -G=-G
31 30 subgsubcl SSubGrpGxSASx-GAS
32 10 25 29 31 syl3anc GTopGrpSSubGrpGAintJSxSx-GAS
33 12 32 sseldd GTopGrpSSubGrpGAintJSxSx-GABaseG
34 eqid yBaseGx-GA+Gy=yBaseGx-GA+Gy
35 eqid +G=+G
36 34 3 35 1 tgplacthmeo GTopGrpx-GABaseGyBaseGx-GA+GyJHomeoJ
37 24 33 36 syl2anc GTopGrpSSubGrpGAintJSxSyBaseGx-GA+GyJHomeoJ
38 hmeoima yBaseGx-GA+GyJHomeoJintJSJyBaseGx-GA+GyintJSJ
39 37 18 38 syl2anc GTopGrpSSubGrpGAintJSxSyBaseGx-GA+GyintJSJ
40 23 39 eqeltrrd GTopGrpSSubGrpGAintJSxSranyintJSx-GA+GyJ
41 tgpgrp GTopGrpGGrp
42 24 41 syl GTopGrpSSubGrpGAintJSxSGGrp
43 11 3ad2ant2 GTopGrpSSubGrpGAintJSSBaseG
44 43 sselda GTopGrpSSubGrpGAintJSxSxBaseG
45 20 28 sseldd GTopGrpSSubGrpGAintJSxSABaseG
46 3 35 30 grpnpcan GGrpxBaseGABaseGx-GA+GA=x
47 42 44 45 46 syl3anc GTopGrpSSubGrpGAintJSxSx-GA+GA=x
48 ovex x-GA+GAV
49 eqid yintJSx-GA+Gy=yintJSx-GA+Gy
50 oveq2 y=Ax-GA+Gy=x-GA+GA
51 49 50 elrnmpt1s AintJSx-GA+GAVx-GA+GAranyintJSx-GA+Gy
52 28 48 51 sylancl GTopGrpSSubGrpGAintJSxSx-GA+GAranyintJSx-GA+Gy
53 47 52 eqeltrrd GTopGrpSSubGrpGAintJSxSxranyintJSx-GA+Gy
54 10 adantr GTopGrpSSubGrpGAintJSxSyintJSSSubGrpG
55 32 adantr GTopGrpSSubGrpGAintJSxSyintJSx-GAS
56 27 sselda GTopGrpSSubGrpGAintJSxSyintJSyS
57 35 subgcl SSubGrpGx-GASySx-GA+GyS
58 54 55 56 57 syl3anc GTopGrpSSubGrpGAintJSxSyintJSx-GA+GyS
59 58 fmpttd GTopGrpSSubGrpGAintJSxSyintJSx-GA+Gy:intJSS
60 59 frnd GTopGrpSSubGrpGAintJSxSranyintJSx-GA+GyS
61 eleq2 u=ranyintJSx-GA+GyxuxranyintJSx-GA+Gy
62 sseq1 u=ranyintJSx-GA+GyuSranyintJSx-GA+GyS
63 61 62 anbi12d u=ranyintJSx-GA+GyxuuSxranyintJSx-GA+GyranyintJSx-GA+GyS
64 63 rspcev ranyintJSx-GA+GyJxranyintJSx-GA+GyranyintJSx-GA+GySuJxuuS
65 40 53 60 64 syl12anc GTopGrpSSubGrpGAintJSxSuJxuuS
66 65 ralrimiva GTopGrpSSubGrpGAintJSxSuJxuuS
67 eltop2 JTopSJxSuJxuuS
68 8 67 syl GTopGrpSSubGrpGAintJSSJxSuJxuuS
69 66 68 mpbird GTopGrpSSubGrpGAintJSSJ