Step | Hyp | Ref
| Expression |
1 | | subgntr.h |
. . . . . . 7
⊢ 𝐽 = (TopOpen‘𝐺) |
2 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
3 | 1, 2 | tgptopon 21886 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈
(TopOn‘(Base‘𝐺))) |
4 | 3 | adantr 481 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐽 ∈ (TopOn‘(Base‘𝐺))) |
5 | | topontop 20718 |
. . . . 5
⊢ (𝐽 ∈
(TopOn‘(Base‘𝐺)) → 𝐽 ∈ Top) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐽 ∈ Top) |
7 | 2 | subgss 17595 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
8 | 7 | adantl 482 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (Base‘𝐺)) |
9 | | toponuni 20719 |
. . . . . 6
⊢ (𝐽 ∈
(TopOn‘(Base‘𝐺)) → (Base‘𝐺) = ∪ 𝐽) |
10 | 4, 9 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (Base‘𝐺) = ∪
𝐽) |
11 | 8, 10 | sseqtrd 3641 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ ∪ 𝐽) |
12 | | eqid 2622 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
13 | 12 | clsss3 20863 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽) |
14 | 6, 11, 13 | syl2anc 693 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ⊆ ∪ 𝐽) |
15 | 14, 10 | sseqtr4d 3642 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ⊆ (Base‘𝐺)) |
16 | 12 | sscls 20860 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ 𝑆 ⊆
((cls‘𝐽)‘𝑆)) |
17 | 6, 11, 16 | syl2anc 693 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) |
18 | | eqid 2622 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
19 | 18 | subg0cl 17602 |
. . . . 5
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑆) |
20 | 19 | adantl 482 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(0g‘𝐺)
∈ 𝑆) |
21 | | ne0i 3921 |
. . . 4
⊢
((0g‘𝐺) ∈ 𝑆 → 𝑆 ≠ ∅) |
22 | 20, 21 | syl 17 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ≠ ∅) |
23 | | ssn0 3976 |
. . 3
⊢ ((𝑆 ⊆ ((cls‘𝐽)‘𝑆) ∧ 𝑆 ≠ ∅) → ((cls‘𝐽)‘𝑆) ≠ ∅) |
24 | 17, 22, 23 | syl2anc 693 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ≠ ∅) |
25 | | df-ov 6653 |
. . . 4
⊢ (𝑥(-g‘𝐺)𝑦) = ((-g‘𝐺)‘〈𝑥, 𝑦〉) |
26 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆)) → 〈𝑥, 𝑦〉 ∈ (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆))) |
27 | | txcls 21407 |
. . . . . . . . . 10
⊢ (((𝐽 ∈
(TopOn‘(Base‘𝐺)) ∧ 𝐽 ∈ (TopOn‘(Base‘𝐺))) ∧ (𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ⊆ (Base‘𝐺))) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) = (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆))) |
28 | 4, 4, 8, 8, 27 | syl22anc 1327 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) = (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆))) |
29 | | txtopon 21394 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈
(TopOn‘(Base‘𝐺)) ∧ 𝐽 ∈ (TopOn‘(Base‘𝐺))) → (𝐽 ×t 𝐽) ∈ (TopOn‘((Base‘𝐺) × (Base‘𝐺)))) |
30 | 4, 4, 29 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐽 ×t 𝐽) ∈ (TopOn‘((Base‘𝐺) × (Base‘𝐺)))) |
31 | | topontop 20718 |
. . . . . . . . . . . 12
⊢ ((𝐽 ×t 𝐽) ∈
(TopOn‘((Base‘𝐺) × (Base‘𝐺))) → (𝐽 ×t 𝐽) ∈ Top) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐽 ×t 𝐽) ∈ Top) |
33 | | cnvimass 5485 |
. . . . . . . . . . . . 13
⊢ (◡(-g‘𝐺) “ 𝑆) ⊆ dom (-g‘𝐺) |
34 | | tgpgrp 21882 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐺 ∈ Grp) |
36 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(-g‘𝐺) = (-g‘𝐺) |
37 | 2, 36 | grpsubf 17494 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ Grp →
(-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺)) |
38 | 35, 37 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺)) |
39 | | fdm 6051 |
. . . . . . . . . . . . . 14
⊢
((-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → dom (-g‘𝐺) = ((Base‘𝐺) × (Base‘𝐺))) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → dom
(-g‘𝐺) =
((Base‘𝐺) ×
(Base‘𝐺))) |
41 | 33, 40 | syl5sseq 3653 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (◡(-g‘𝐺) “ 𝑆) ⊆ ((Base‘𝐺) × (Base‘𝐺))) |
42 | | toponuni 20719 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ×t 𝐽) ∈
(TopOn‘((Base‘𝐺) × (Base‘𝐺))) → ((Base‘𝐺) × (Base‘𝐺)) = ∪ (𝐽 ×t 𝐽)) |
43 | 30, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((Base‘𝐺) × (Base‘𝐺)) = ∪ (𝐽
×t 𝐽)) |
44 | 41, 43 | sseqtrd 3641 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (◡(-g‘𝐺) “ 𝑆) ⊆ ∪
(𝐽 ×t
𝐽)) |
45 | 36 | subgsubcl 17605 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥(-g‘𝐺)𝑦) ∈ 𝑆) |
46 | 45 | 3expb 1266 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(-g‘𝐺)𝑦) ∈ 𝑆) |
47 | 46 | ralrimivva 2971 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(-g‘𝐺)𝑦) ∈ 𝑆) |
48 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((-g‘𝐺)‘𝑧) = ((-g‘𝐺)‘〈𝑥, 𝑦〉)) |
49 | 48, 25 | syl6eqr 2674 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((-g‘𝐺)‘𝑧) = (𝑥(-g‘𝐺)𝑦)) |
50 | 49 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((-g‘𝐺)‘𝑧) ∈ 𝑆 ↔ (𝑥(-g‘𝐺)𝑦) ∈ 𝑆)) |
51 | 50 | ralxp 5263 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
(𝑆 × 𝑆)((-g‘𝐺)‘𝑧) ∈ 𝑆 ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(-g‘𝐺)𝑦) ∈ 𝑆) |
52 | 47, 51 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∀𝑧 ∈ (𝑆 × 𝑆)((-g‘𝐺)‘𝑧) ∈ 𝑆) |
53 | 52 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ∀𝑧 ∈ (𝑆 × 𝑆)((-g‘𝐺)‘𝑧) ∈ 𝑆) |
54 | | ffun 6048 |
. . . . . . . . . . . . . 14
⊢
((-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → Fun (-g‘𝐺)) |
55 | 38, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → Fun
(-g‘𝐺)) |
56 | | xpss12 5225 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ⊆ (Base‘𝐺)) → (𝑆 × 𝑆) ⊆ ((Base‘𝐺) × (Base‘𝐺))) |
57 | 8, 8, 56 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 × 𝑆) ⊆ ((Base‘𝐺) × (Base‘𝐺))) |
58 | 57, 40 | sseqtr4d 3642 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 × 𝑆) ⊆ dom (-g‘𝐺)) |
59 | | funimass5 6334 |
. . . . . . . . . . . . 13
⊢ ((Fun
(-g‘𝐺)
∧ (𝑆 × 𝑆) ⊆ dom
(-g‘𝐺))
→ ((𝑆 × 𝑆) ⊆ (◡(-g‘𝐺) “ 𝑆) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)((-g‘𝐺)‘𝑧) ∈ 𝑆)) |
60 | 55, 58, 59 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((𝑆 × 𝑆) ⊆ (◡(-g‘𝐺) “ 𝑆) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)((-g‘𝐺)‘𝑧) ∈ 𝑆)) |
61 | 53, 60 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 × 𝑆) ⊆ (◡(-g‘𝐺) “ 𝑆)) |
62 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
63 | 62 | clsss 20858 |
. . . . . . . . . . 11
⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ (◡(-g‘𝐺) “ 𝑆) ⊆ ∪
(𝐽 ×t
𝐽) ∧ (𝑆 × 𝑆) ⊆ (◡(-g‘𝐺) “ 𝑆)) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) ⊆ ((cls‘(𝐽 ×t 𝐽))‘(◡(-g‘𝐺) “ 𝑆))) |
64 | 32, 44, 61, 63 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) ⊆ ((cls‘(𝐽 ×t 𝐽))‘(◡(-g‘𝐺) “ 𝑆))) |
65 | 1, 36 | tgpsubcn 21894 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ TopGrp →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
66 | 65 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(-g‘𝐺)
∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
67 | 12 | cncls2i 21074 |
. . . . . . . . . . 11
⊢
(((-g‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ 𝑆 ⊆ ∪ 𝐽) → ((cls‘(𝐽 ×t 𝐽))‘(◡(-g‘𝐺) “ 𝑆)) ⊆ (◡(-g‘𝐺) “ ((cls‘𝐽)‘𝑆))) |
68 | 66, 11, 67 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘(𝐽 ×t 𝐽))‘(◡(-g‘𝐺) “ 𝑆)) ⊆ (◡(-g‘𝐺) “ ((cls‘𝐽)‘𝑆))) |
69 | 64, 68 | sstrd 3613 |
. . . . . . . . 9
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘(𝐽 ×t 𝐽))‘(𝑆 × 𝑆)) ⊆ (◡(-g‘𝐺) “ ((cls‘𝐽)‘𝑆))) |
70 | 28, 69 | eqsstr3d 3640 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆)) ⊆ (◡(-g‘𝐺) “ ((cls‘𝐽)‘𝑆))) |
71 | 70 | sselda 3603 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 〈𝑥, 𝑦〉 ∈ (((cls‘𝐽)‘𝑆) × ((cls‘𝐽)‘𝑆))) → 〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐺) “ ((cls‘𝐽)‘𝑆))) |
72 | 26, 71 | sylan2 491 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → 〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐺) “ ((cls‘𝐽)‘𝑆))) |
73 | 34 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → 𝐺 ∈ Grp) |
74 | | ffn 6045 |
. . . . . . 7
⊢
((-g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → (-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺))) |
75 | | elpreima 6337 |
. . . . . . 7
⊢
((-g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐺) “ ((cls‘𝐽)‘𝑆)) ↔ (〈𝑥, 𝑦〉 ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ ((cls‘𝐽)‘𝑆)))) |
76 | 73, 37, 74, 75 | 4syl 19 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → (〈𝑥, 𝑦〉 ∈ (◡(-g‘𝐺) “ ((cls‘𝐽)‘𝑆)) ↔ (〈𝑥, 𝑦〉 ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ ((cls‘𝐽)‘𝑆)))) |
77 | 72, 76 | mpbid 222 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → (〈𝑥, 𝑦〉 ∈ ((Base‘𝐺) × (Base‘𝐺)) ∧ ((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ ((cls‘𝐽)‘𝑆))) |
78 | 77 | simprd 479 |
. . . 4
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → ((-g‘𝐺)‘〈𝑥, 𝑦〉) ∈ ((cls‘𝐽)‘𝑆)) |
79 | 25, 78 | syl5eqel 2705 |
. . 3
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((cls‘𝐽)‘𝑆))) → (𝑥(-g‘𝐺)𝑦) ∈ ((cls‘𝐽)‘𝑆)) |
80 | 79 | ralrimivva 2971 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ∀𝑥 ∈ ((cls‘𝐽)‘𝑆)∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(-g‘𝐺)𝑦) ∈ ((cls‘𝐽)‘𝑆)) |
81 | 2, 36 | issubg4 17613 |
. . 3
⊢ (𝐺 ∈ Grp →
(((cls‘𝐽)‘𝑆) ∈ (SubGrp‘𝐺) ↔ (((cls‘𝐽)‘𝑆) ⊆ (Base‘𝐺) ∧ ((cls‘𝐽)‘𝑆) ≠ ∅ ∧ ∀𝑥 ∈ ((cls‘𝐽)‘𝑆)∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(-g‘𝐺)𝑦) ∈ ((cls‘𝐽)‘𝑆)))) |
82 | 35, 81 | syl 17 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (((cls‘𝐽)‘𝑆) ∈ (SubGrp‘𝐺) ↔ (((cls‘𝐽)‘𝑆) ⊆ (Base‘𝐺) ∧ ((cls‘𝐽)‘𝑆) ≠ ∅ ∧ ∀𝑥 ∈ ((cls‘𝐽)‘𝑆)∀𝑦 ∈ ((cls‘𝐽)‘𝑆)(𝑥(-g‘𝐺)𝑦) ∈ ((cls‘𝐽)‘𝑆)))) |
83 | 15, 24, 80, 82 | mpbir3and 1245 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (SubGrp‘𝐺)) |