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 ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion subgntr ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 subgntr.h ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 df-ima ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) “ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) = ran ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
3 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 1 3 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
5 4 3ad2ant1 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
6 5 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
7 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → 𝐽 ∈ Top )
8 5 7 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝐽 ∈ Top )
9 8 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐽 ∈ Top )
10 simpl2 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
11 3 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
12 10 11 syl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
13 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
14 6 13 syl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
15 12 14 sseqtrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ⊆ ∪ 𝐽 )
16 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
17 16 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 )
18 9 15 17 syl2anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 )
19 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 ) )
20 6 18 19 syl2anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 ) )
21 20 resmptd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) = ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) )
22 21 rneqd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ran ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) = ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) )
23 2 22 eqtrid ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) “ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) = ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) )
24 simpl1 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐺 ∈ TopGrp )
25 simpr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
26 16 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 )
27 9 15 26 syl2anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 )
28 simpl3 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
29 27 28 sseldd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
30 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
31 30 subgsubcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ∈ 𝑆 )
32 10 25 29 31 syl3anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ∈ 𝑆 )
33 12 32 sseldd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ∈ ( Base ‘ 𝐺 ) )
34 eqid ⊢ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) )
35 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
36 34 3 35 1 tgplacthmeo ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
37 24 33 36 syl2anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
38 hmeoima ⊢ ( ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( 𝐽 Homeo 𝐽 ) ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) “ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 )
39 37 18 38 syl2anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) “ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ 𝐽 )
40 23 39 eqeltrrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ 𝐽 )
41 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
42 24 41 syl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐺 ∈ Grp )
43 11 3ad2ant2 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
44 43 sselda ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
45 20 28 sseldd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
46 3 35 30 grpnpcan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝐴 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) = 𝑥 )
47 42 44 45 46 syl3anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) = 𝑥 )
48 ovex ⊢ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ∈ V
49 eqid ⊢ ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) )
50 oveq2 ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) = ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) )
51 49 50 elrnmpt1s ⊢ ( ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ∈ V ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ∈ ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) )
52 28 48 51 sylancl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ∈ ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) )
53 47 52 eqeltrrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) )
54 10 adantr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
55 32 adantr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ∈ 𝑆 )
56 27 sselda ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
57 35 subgcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
58 54 55 56 57 syl3anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
59 58 fmpttd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) : ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⟶ 𝑆 )
60 59 frnd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ 𝑆 )
61 eleq2 ⊢ ( 𝑢 = ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ) )
62 sseq1 ⊢ ( 𝑢 = ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) → ( 𝑢 ⊆ 𝑆 ↔ ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ 𝑆 ) )
63 61 62 anbi12d ⊢ ( 𝑢 = ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) → ( ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑆 ) ↔ ( 𝑥 ∈ ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ∧ ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ 𝑆 ) ) )
64 63 rspcev ⊢ ( ( ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ 𝐽 ∧ ( 𝑥 ∈ ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ∧ ran ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝐴 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ 𝑆 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑆 ) )
65 40 53 60 64 syl12anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑆 ) )
66 65 ralrimiva ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑆 ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑆 ) )
67 eltop2 ⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝑆 ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑆 ) ) )
68 8 67 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑆 ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝑆 ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑆 ) ) )
69 66 68 mpbird ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ∈ 𝐽 )