| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | subgtgp.h | . . . 4
⊢ 𝐻 = (𝐺 ↾s 𝑆) | 
| 2 | 1 | subggrp 19147 | . . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) | 
| 3 | 2 | adantl 481 | . 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Grp) | 
| 4 |  | tgptmd 24087 | . . 3
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd) | 
| 5 |  | subgsubm 19166 | . . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (SubMnd‘𝐺)) | 
| 6 | 1 | submtmd 24112 | . . 3
⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopMnd) | 
| 7 | 4, 5, 6 | syl2an 596 | . 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopMnd) | 
| 8 | 1 | subgbas 19148 | . . . . . . 7
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻)) | 
| 9 | 8 | adantl 481 | . . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 = (Base‘𝐻)) | 
| 10 | 9 | mpteq1d 5237 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ 𝑆 ↦ ((invg‘𝐻)‘𝑥)) = (𝑥 ∈ (Base‘𝐻) ↦ ((invg‘𝐻)‘𝑥))) | 
| 11 |  | eqid 2737 | . . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 12 |  | eqid 2737 | . . . . . . . 8
⊢
(invg‘𝐻) = (invg‘𝐻) | 
| 13 | 1, 11, 12 | subginv 19151 | . . . . . . 7
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐺)‘𝑥) = ((invg‘𝐻)‘𝑥)) | 
| 14 | 13 | adantll 714 | . . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐺)‘𝑥) = ((invg‘𝐻)‘𝑥)) | 
| 15 | 14 | mpteq2dva 5242 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ 𝑆 ↦ ((invg‘𝐺)‘𝑥)) = (𝑥 ∈ 𝑆 ↦ ((invg‘𝐻)‘𝑥))) | 
| 16 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 17 | 16, 12 | grpinvf 19004 | . . . . . . 7
⊢ (𝐻 ∈ Grp →
(invg‘𝐻):(Base‘𝐻)⟶(Base‘𝐻)) | 
| 18 | 3, 17 | syl 17 | . . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻):(Base‘𝐻)⟶(Base‘𝐻)) | 
| 19 | 18 | feqmptd 6977 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻) =
(𝑥 ∈ (Base‘𝐻) ↦
((invg‘𝐻)‘𝑥))) | 
| 20 | 10, 15, 19 | 3eqtr4rd 2788 | . . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻) =
(𝑥 ∈ 𝑆 ↦ ((invg‘𝐺)‘𝑥))) | 
| 21 |  | eqid 2737 | . . . . 5
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
((TopOpen‘𝐺)
↾t 𝑆) | 
| 22 |  | eqid 2737 | . . . . . . 7
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) | 
| 23 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 24 | 22, 23 | tgptopon 24090 | . . . . . 6
⊢ (𝐺 ∈ TopGrp →
(TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) | 
| 25 | 24 | adantr 480 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) | 
| 26 | 23 | subgss 19145 | . . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) | 
| 27 | 26 | adantl 481 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (Base‘𝐺)) | 
| 28 |  | tgpgrp 24086 | . . . . . . . . 9
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) | 
| 29 | 28 | adantr 480 | . . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐺 ∈ Grp) | 
| 30 | 23, 11 | grpinvf 19004 | . . . . . . . 8
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) | 
| 31 | 29, 30 | syl 17 | . . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) | 
| 32 | 31 | feqmptd 6977 | . . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐺) =
(𝑥 ∈ (Base‘𝐺) ↦
((invg‘𝐺)‘𝑥))) | 
| 33 | 22, 11 | tgpinv 24093 | . . . . . . 7
⊢ (𝐺 ∈ TopGrp →
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn (TopOpen‘𝐺))) | 
| 34 | 33 | adantr 480 | . . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn (TopOpen‘𝐺))) | 
| 35 | 32, 34 | eqeltrrd 2842 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥)) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))) | 
| 36 | 21, 25, 27, 35 | cnmpt1res 23684 | . . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ 𝑆 ↦ ((invg‘𝐺)‘𝑥)) ∈ (((TopOpen‘𝐺) ↾t 𝑆) Cn (TopOpen‘𝐺))) | 
| 37 | 20, 36 | eqeltrd 2841 | . . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
(TopOpen‘𝐺))) | 
| 38 | 18 | frnd 6744 | . . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ran
(invg‘𝐻)
⊆ (Base‘𝐻)) | 
| 39 | 38, 9 | sseqtrrd 4021 | . . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ran
(invg‘𝐻)
⊆ 𝑆) | 
| 40 |  | cnrest2 23294 | . . . 4
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ ran (invg‘𝐻) ⊆ 𝑆 ∧ 𝑆 ⊆ (Base‘𝐺)) → ((invg‘𝐻) ∈ (((TopOpen‘𝐺) ↾t 𝑆) Cn (TopOpen‘𝐺)) ↔
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆)))) | 
| 41 | 25, 39, 27, 40 | syl3anc 1373 | . . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
((invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
(TopOpen‘𝐺)) ↔
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆)))) | 
| 42 | 37, 41 | mpbid 232 | . 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) →
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆))) | 
| 43 | 1, 22 | resstopn 23194 | . . 3
⊢
((TopOpen‘𝐺)
↾t 𝑆) =
(TopOpen‘𝐻) | 
| 44 | 43, 12 | istgp 24085 | . 2
⊢ (𝐻 ∈ TopGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ TopMnd ∧
(invg‘𝐻)
∈ (((TopOpen‘𝐺)
↾t 𝑆) Cn
((TopOpen‘𝐺)
↾t 𝑆)))) | 
| 45 | 3, 7, 42, 44 | syl3anbrc 1344 | 1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopGrp) |