Metamath Proof Explorer


Theorem clsnsg

Description: The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis subgntr.h 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion clsnsg ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( NrmSGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 subgntr.h 𝐽 = ( TopOpen ‘ 𝐺 )
2 nsgsubg ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
3 1 clssubg ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )
4 2 3 sylan2 ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )
5 df-ima ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ran ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ↾ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
6 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7 1 6 tgptopon ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
8 7 ad2antrr ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
9 topontop ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → 𝐽 ∈ Top )
10 8 9 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝐽 ∈ Top )
11 2 ad2antlr ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
12 6 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
13 11 12 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
14 toponuni ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = 𝐽 )
15 8 14 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = 𝐽 )
16 13 15 sseqtrd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑆 𝐽 )
17 eqid 𝐽 = 𝐽
18 17 clsss3 ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝐽 )
19 10 16 18 syl2anc ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝐽 )
20 19 15 sseqtrrd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 ) )
21 20 resmptd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ↾ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) )
22 21 rneqd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ran ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ↾ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ran ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) )
23 5 22 syl5eq ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ran ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) )
24 eqid ( +g𝐺 ) = ( +g𝐺 )
25 tgptmd ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
26 25 ad2antrr ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝐺 ∈ TopMnd )
27 simpr ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
28 8 8 27 cnmptc ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
29 8 cnmptid ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ 𝑦 ) ∈ ( 𝐽 Cn 𝐽 ) )
30 1 24 26 8 28 29 cnmpt1plusg ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
31 eqid ( -g𝐺 ) = ( -g𝐺 )
32 1 31 tgpsubcn ( 𝐺 ∈ TopGrp → ( -g𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
33 32 ad2antrr ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( -g𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
34 8 30 28 33 cnmpt12f ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
35 17 cnclsi ( ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑆 𝐽 ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ 𝑆 ) ) )
36 34 16 35 syl2anc ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ 𝑆 ) ) )
37 df-ima ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ 𝑆 ) = ran ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ↾ 𝑆 )
38 13 resmptd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ↾ 𝑆 ) = ( 𝑦𝑆 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) )
39 38 rneqd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ran ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ↾ 𝑆 ) = ran ( 𝑦𝑆 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) )
40 37 39 syl5eq ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ 𝑆 ) = ran ( 𝑦𝑆 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) )
41 6 24 31 nsgconj ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦𝑆 ) → ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ 𝑆 )
42 41 ad4ant234 ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦𝑆 ) → ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ 𝑆 )
43 42 fmpttd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦𝑆 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) : 𝑆𝑆 )
44 43 frnd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ran ( 𝑦𝑆 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ⊆ 𝑆 )
45 40 44 eqsstrd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ 𝑆 ) ⊆ 𝑆 )
46 17 clsss ( ( 𝐽 ∈ Top ∧ 𝑆 𝐽 ∧ ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ 𝑆 ) ⊆ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
47 10 16 45 46 syl3anc ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
48 36 47 sstrd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
49 23 48 eqsstrrd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ran ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
50 ovex ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ V
51 eqid ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) = ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) )
52 50 51 fnmpti ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) Fn ( ( cls ‘ 𝐽 ) ‘ 𝑆 )
53 df-f ( ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) : ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⟶ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) Fn ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ ran ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
54 52 53 mpbiran ( ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) : ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⟶ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ran ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
55 49 54 sylibr ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) : ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⟶ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
56 51 fmpt ( ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↦ ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ) : ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⟶ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
57 55 56 sylibr ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
58 57 ralrimiva ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
59 6 24 31 isnsg3 ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ( -g𝐺 ) 𝑥 ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
60 4 58 59 sylanbrc ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( NrmSGrp ‘ 𝐺 ) )