Metamath Proof Explorer

Theorem clssubg

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

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

Proof

Step Hyp Ref Expression
1 subgntr.h ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 1 2 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
4 3 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
5 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → 𝐽 ∈ Top )
6 4 5 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐽 ∈ Top )
7 2 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
8 7 adantl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
9 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
10 4 9 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
11 8 10 sseqtrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ∪ 𝐽 )
12 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
13 12 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 )
14 6 11 13 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 )
15 14 10 sseqtrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 ) )
16 12 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
17 6 11 16 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
18 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
19 18 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
20 19 adantl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
21 20 ne0d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ≠ ∅ )
22 ssn0 ⊢ ( ( 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑆 ≠ ∅ ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ≠ ∅ )
23 17 21 22 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ≠ ∅ )
24 df-ov ⊢ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
25 opelxpi ⊢ ( ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) × ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
26 txcls ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( 𝑆 × 𝑆 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) × ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
27 4 4 8 8 26 syl22anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( 𝑆 × 𝑆 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) × ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
28 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ) → ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) )
29 4 4 28 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) )
30 topontop ⊢ ( ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) → ( 𝐽 ×t 𝐽 ) ∈ Top )
31 29 30 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐽 ×t 𝐽 ) ∈ Top )
32 cnvimass ⊢ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ⊆ dom ( -g ‘ 𝐺 )
33 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
34 33 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐺 ∈ Grp )
35 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
36 2 35 grpsubf ⊢ ( 𝐺 ∈ Grp → ( -g ‘ 𝐺 ) : ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ⟶ ( Base ‘ 𝐺 ) )
37 34 36 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( -g ‘ 𝐺 ) : ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ⟶ ( Base ‘ 𝐺 ) )
38 32 37 fssdm ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ⊆ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
39 toponuni ⊢ ( ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) → ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) = ∪ ( 𝐽 ×t 𝐽 ) )
40 29 39 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) = ∪ ( 𝐽 ×t 𝐽 ) )
41 38 40 sseqtrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ⊆ ∪ ( 𝐽 ×t 𝐽 ) )
42 35 subgsubcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
43 42 3expb ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
44 43 ralrimivva ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
45 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( -g ‘ 𝐺 ) ‘ 𝑧 ) = ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
46 45 24 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( -g ‘ 𝐺 ) ‘ 𝑧 ) = ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) )
47 46 eleq1d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( -g ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 ↔ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) )
48 47 ralxp ⊢ ( ∀ 𝑧 ∈ ( 𝑆 × 𝑆 ) ( ( -g ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
49 44 48 sylibr ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑧 ∈ ( 𝑆 × 𝑆 ) ( ( -g ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 )
50 49 adantl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ∀ 𝑧 ∈ ( 𝑆 × 𝑆 ) ( ( -g ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 )
51 37 ffund ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → Fun ( -g ‘ 𝐺 ) )
52 xpss12 ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑆 × 𝑆 ) ⊆ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
53 8 8 52 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 × 𝑆 ) ⊆ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
54 37 fdmd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → dom ( -g ‘ 𝐺 ) = ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
55 53 54 sseqtrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 × 𝑆 ) ⊆ dom ( -g ‘ 𝐺 ) )
56 funimass5 ⊢ ( ( Fun ( -g ‘ 𝐺 ) ∧ ( 𝑆 × 𝑆 ) ⊆ dom ( -g ‘ 𝐺 ) ) → ( ( 𝑆 × 𝑆 ) ⊆ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ↔ ∀ 𝑧 ∈ ( 𝑆 × 𝑆 ) ( ( -g ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 ) )
57 51 55 56 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 × 𝑆 ) ⊆ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ↔ ∀ 𝑧 ∈ ( 𝑆 × 𝑆 ) ( ( -g ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑆 ) )
58 50 57 mpbird ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 × 𝑆 ) ⊆ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) )
59 eqid ⊢ ∪ ( 𝐽 ×t 𝐽 ) = ∪ ( 𝐽 ×t 𝐽 )
60 59 clsss ⊢ ( ( ( 𝐽 ×t 𝐽 ) ∈ Top ∧ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ⊆ ∪ ( 𝐽 ×t 𝐽 ) ∧ ( 𝑆 × 𝑆 ) ⊆ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( 𝑆 × 𝑆 ) ) ⊆ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ) )
61 31 41 58 60 syl3anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( 𝑆 × 𝑆 ) ) ⊆ ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ) )
62 1 35 tgpsubcn ⊢ ( 𝐺 ∈ TopGrp → ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
63 62 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
64 12 cncls2i ⊢ ( ( ( -g ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ) ⊆ ( ◡ ( -g ‘ 𝐺 ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
65 63 11 64 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( ◡ ( -g ‘ 𝐺 ) “ 𝑆 ) ) ⊆ ( ◡ ( -g ‘ 𝐺 ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
66 61 65 sstrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ ( 𝑆 × 𝑆 ) ) ⊆ ( ◡ ( -g ‘ 𝐺 ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
67 27 66 eqsstrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) × ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ◡ ( -g ‘ 𝐺 ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
68 67 sselda ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) × ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐺 ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
69 25 68 sylan2 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐺 ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
70 33 ad2antrr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → 𝐺 ∈ Grp )
71 ffn ⊢ ( ( -g ‘ 𝐺 ) : ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ⟶ ( Base ‘ 𝐺 ) → ( -g ‘ 𝐺 ) Fn ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
72 elpreima ⊢ ( ( -g ‘ 𝐺 ) Fn ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐺 ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ∧ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
73 70 36 71 72 4syl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( -g ‘ 𝐺 ) “ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ∧ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
74 69 73 mpbid ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ∧ ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
75 74 simprd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ( -g ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
76 24 75 eqeltrid ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
77 76 ralrimivva ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ∀ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
78 2 35 issubg4 ⊢ ( 𝐺 ∈ Grp → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
79 34 78 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝐺 ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∀ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
80 15 23 77 79 mpbir3and ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )