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 ‘ 𝐺 ) )