Step | Hyp | Ref
| Expression |
1 | | subgtgp.h |
. . . 4
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
2 | 1 | subggrp 18758 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
3 | 2 | adantl 482 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Grp) |
4 | | tgptmd 23230 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd) |
5 | | subgsubm 18777 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (SubMnd‘𝐺)) |
6 | 1 | submtmd 23255 |
. . 3
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopMnd) |
7 | 4, 5, 6 | syl2an 596 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopMnd) |
8 | 1 | subgbas 18759 |
. . . . . . 7
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻)) |
9 | 8 | adantl 482 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 = (Base‘𝐻)) |
10 | 9 | mpteq1d 5169 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ 𝑆 ↦ ((invg‘𝐻)‘𝑥)) = (𝑥 ∈ (Base‘𝐻) ↦ ((invg‘𝐻)‘𝑥))) |
11 | | eqid 2738 |
. . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) |
12 | | eqid 2738 |
. . . . . . . 8
⊢
(invg‘𝐻) = (invg‘𝐻) |
13 | 1, 11, 12 | subginv 18762 |
. . . . . . 7
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐺)‘𝑥) = ((invg‘𝐻)‘𝑥)) |
14 | 13 | adantll 711 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐺)‘𝑥) = ((invg‘𝐻)‘𝑥)) |
15 | 14 | mpteq2dva 5174 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ 𝑆 ↦ ((invg‘𝐺)‘𝑥)) = (𝑥 ∈ 𝑆 ↦ ((invg‘𝐻)‘𝑥))) |
16 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘𝐻) =
(Base‘𝐻) |
17 | 16, 12 | grpinvf 18626 |
. . . . . . 7
⊢ (𝐻 ∈ Grp →
(invg‘𝐻):(Base‘𝐻)⟶(Base‘𝐻)) |
18 | 3, 17 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻):(Base‘𝐻)⟶(Base‘𝐻)) |
19 | 18 | feqmptd 6837 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻) =
(𝑥 ∈ (Base‘𝐻) ↦
((invg‘𝐻)‘𝑥))) |
20 | 10, 15, 19 | 3eqtr4rd 2789 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻) =
(𝑥 ∈ 𝑆 ↦ ((invg‘𝐺)‘𝑥))) |
21 | | eqid 2738 |
. . . . 5
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
((TopOpen‘𝐺)
↾t 𝑆) |
22 | | eqid 2738 |
. . . . . . 7
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
23 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
24 | 22, 23 | tgptopon 23233 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp →
(TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) |
25 | 24 | adantr 481 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) |
26 | 23 | subgss 18756 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
27 | 26 | adantl 482 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (Base‘𝐺)) |
28 | | tgpgrp 23229 |
. . . . . . . . 9
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
29 | 28 | adantr 481 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐺 ∈ Grp) |
30 | 23, 11 | grpinvf 18626 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
32 | 31 | feqmptd 6837 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐺) =
(𝑥 ∈ (Base‘𝐺) ↦
((invg‘𝐺)‘𝑥))) |
33 | 22, 11 | tgpinv 23236 |
. . . . . . 7
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn (TopOpen‘𝐺))) |
34 | 33 | adantr 481 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn (TopOpen‘𝐺))) |
35 | 32, 34 | eqeltrrd 2840 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥)) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))) |
36 | 21, 25, 27, 35 | cnmpt1res 22827 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ 𝑆 ↦ ((invg‘𝐺)‘𝑥)) ∈ (((TopOpen‘𝐺) ↾t 𝑆) Cn (TopOpen‘𝐺))) |
37 | 20, 36 | eqeltrd 2839 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
(TopOpen‘𝐺))) |
38 | 18 | frnd 6608 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ran
(invg‘𝐻)
⊆ (Base‘𝐻)) |
39 | 38, 9 | sseqtrrd 3962 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ran
(invg‘𝐻)
⊆ 𝑆) |
40 | | cnrest2 22437 |
. . . 4
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ ran (invg‘𝐻) ⊆ 𝑆 ∧ 𝑆 ⊆ (Base‘𝐺)) → ((invg‘𝐻) ∈ (((TopOpen‘𝐺) ↾t 𝑆) Cn (TopOpen‘𝐺)) ↔
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆)))) |
41 | 25, 39, 27, 40 | syl3anc 1370 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
((invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
(TopOpen‘𝐺)) ↔
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆)))) |
42 | 37, 41 | mpbid 231 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆))) |
43 | 1, 22 | resstopn 22337 |
. . 3
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
(TopOpen‘𝐻) |
44 | 43, 12 | istgp 23228 |
. 2
⊢ (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopMnd ∧
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆)))) |
45 | 3, 7, 42, 44 | syl3anbrc 1342 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopGrp) |