Step | Hyp | Ref
| Expression |
1 | | subgtgp.h |
. . . 4
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
2 | 1 | subggrp 17420 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
3 | 2 | adantl 481 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Grp) |
4 | | tgptmd 21693 |
. . 3
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd) |
5 | | subgsubm 17439 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (SubMnd‘𝐺)) |
6 | 1 | submtmd 21718 |
. . 3
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopMnd) |
7 | 4, 5, 6 | syl2an 493 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopMnd) |
8 | 1 | subgbas 17421 |
. . . . . . 7
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻)) |
9 | 8 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 = (Base‘𝐻)) |
10 | 9 | mpteq1d 4666 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ 𝑆 ↦ ((invg‘𝐻)‘𝑥)) = (𝑥 ∈ (Base‘𝐻) ↦ ((invg‘𝐻)‘𝑥))) |
11 | | eqid 2610 |
. . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) |
12 | | eqid 2610 |
. . . . . . . 8
⊢
(invg‘𝐻) = (invg‘𝐻) |
13 | 1, 11, 12 | subginv 17424 |
. . . . . . 7
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐺)‘𝑥) = ((invg‘𝐻)‘𝑥)) |
14 | 13 | adantll 746 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐺)‘𝑥) = ((invg‘𝐻)‘𝑥)) |
15 | 14 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ 𝑆 ↦ ((invg‘𝐺)‘𝑥)) = (𝑥 ∈ 𝑆 ↦ ((invg‘𝐻)‘𝑥))) |
16 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝐻) =
(Base‘𝐻) |
17 | 16, 12 | grpinvf 17289 |
. . . . . . 7
⊢ (𝐻 ∈ Grp →
(invg‘𝐻):(Base‘𝐻)⟶(Base‘𝐻)) |
18 | 3, 17 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻):(Base‘𝐻)⟶(Base‘𝐻)) |
19 | 18 | feqmptd 6159 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻) =
(𝑥 ∈ (Base‘𝐻) ↦
((invg‘𝐻)‘𝑥))) |
20 | 10, 15, 19 | 3eqtr4rd 2655 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻) =
(𝑥 ∈ 𝑆 ↦ ((invg‘𝐺)‘𝑥))) |
21 | | eqid 2610 |
. . . . 5
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
((TopOpen‘𝐺)
↾t 𝑆) |
22 | | eqid 2610 |
. . . . . . 7
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
23 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
24 | 22, 23 | tgptopon 21696 |
. . . . . 6
⊢ (𝐺 ∈ TopGrp →
(TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) |
25 | 24 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) |
26 | 23 | subgss 17418 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
27 | 26 | adantl 481 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (Base‘𝐺)) |
28 | | tgpgrp 21692 |
. . . . . . . . 9
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
29 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐺 ∈ Grp) |
30 | 23, 11 | grpinvf 17289 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
32 | 31 | feqmptd 6159 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐺) =
(𝑥 ∈ (Base‘𝐺) ↦
((invg‘𝐺)‘𝑥))) |
33 | 22, 11 | tgpinv 21699 |
. . . . . . 7
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn (TopOpen‘𝐺))) |
34 | 33 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn (TopOpen‘𝐺))) |
35 | 32, 34 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥)) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))) |
36 | 21, 25, 27, 35 | cnmpt1res 21289 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ 𝑆 ↦ ((invg‘𝐺)‘𝑥)) ∈ (((TopOpen‘𝐺) ↾t 𝑆) Cn (TopOpen‘𝐺))) |
37 | 20, 36 | eqeltrd 2688 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
(TopOpen‘𝐺))) |
38 | | frn 5966 |
. . . . . 6
⊢
((invg‘𝐻):(Base‘𝐻)⟶(Base‘𝐻) → ran (invg‘𝐻) ⊆ (Base‘𝐻)) |
39 | 18, 38 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ran
(invg‘𝐻)
⊆ (Base‘𝐻)) |
40 | 39, 9 | sseqtr4d 3605 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ran
(invg‘𝐻)
⊆ 𝑆) |
41 | | cnrest2 20900 |
. . . 4
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ ran (invg‘𝐻) ⊆ 𝑆 ∧ 𝑆 ⊆ (Base‘𝐺)) → ((invg‘𝐻) ∈ (((TopOpen‘𝐺) ↾t 𝑆) Cn (TopOpen‘𝐺)) ↔
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆)))) |
42 | 25, 40, 27, 41 | syl3anc 1318 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
((invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
(TopOpen‘𝐺)) ↔
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆)))) |
43 | 37, 42 | mpbid 221 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆))) |
44 | 1, 22 | resstopn 20800 |
. . 3
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
(TopOpen‘𝐻) |
45 | 44, 12 | istgp 21691 |
. 2
⊢ (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopMnd ∧
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆)))) |
46 | 3, 7, 43, 45 | syl3anbrc 1239 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopGrp) |