Metamath Proof Explorer

Theorem subgtgp

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

Ref Expression
Hypothesis subgtgp.h ⊢ H = G ↾ 𝑠 S
Assertion subgtgp ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → H ∈ TopGrp

Proof

Step Hyp Ref Expression
1 subgtgp.h ⊢ H = G ↾ 𝑠 S
2 1 subggrp ⊢ S ∈ SubGrp ⁡ G → H ∈ Grp
3 2 adantl ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → H ∈ Grp
4 tgptmd ⊢ G ∈ TopGrp → G ∈ TopMnd
5 subgsubm ⊢ S ∈ SubGrp ⁡ G → S ∈ SubMnd ⁡ G
6 1 submtmd ⊢ G ∈ TopMnd ∧ S ∈ SubMnd ⁡ G → H ∈ TopMnd
7 4 5 6 syl2an ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → H ∈ TopMnd
8 1 subgbas ⊢ S ∈ SubGrp ⁡ G → S = Base H
9 8 adantl ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → S = Base H
10 9 mpteq1d ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → x ∈ S ⟼ inv g ⁡ H ⁡ x = x ∈ Base H ⟼ inv g ⁡ H ⁡ x
11 eqid ⊢ inv g ⁡ G = inv g ⁡ G
12 eqid ⊢ inv g ⁡ H = inv g ⁡ H
13 1 11 12 subginv ⊢ S ∈ SubGrp ⁡ G ∧ x ∈ S → inv g ⁡ G ⁡ x = inv g ⁡ H ⁡ x
14 13 adantll ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G ∧ x ∈ S → inv g ⁡ G ⁡ x = inv g ⁡ H ⁡ x
15 14 mpteq2dva ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → x ∈ S ⟼ inv g ⁡ G ⁡ x = x ∈ S ⟼ inv g ⁡ H ⁡ x
16 eqid ⊢ Base H = Base H
17 16 12 grpinvf ⊢ H ∈ Grp → inv g ⁡ H : Base H ⟶ Base H
18 3 17 syl ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → inv g ⁡ H : Base H ⟶ Base H
19 18 feqmptd ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → inv g ⁡ H = x ∈ Base H ⟼ inv g ⁡ H ⁡ x
20 10 15 19 3eqtr4rd ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → inv g ⁡ H = x ∈ S ⟼ inv g ⁡ G ⁡ x
21 eqid ⊢ TopOpen ⁡ G ↾ 𝑡 S = TopOpen ⁡ G ↾ 𝑡 S
22 eqid ⊢ TopOpen ⁡ G = TopOpen ⁡ G
23 eqid ⊢ Base G = Base G
24 22 23 tgptopon ⊢ G ∈ TopGrp → TopOpen ⁡ G ∈ TopOn ⁡ Base G
25 24 adantr ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → TopOpen ⁡ G ∈ TopOn ⁡ Base G
26 23 subgss ⊢ S ∈ SubGrp ⁡ G → S ⊆ Base G
27 26 adantl ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → S ⊆ Base G
28 tgpgrp ⊢ G ∈ TopGrp → G ∈ Grp
29 28 adantr ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → G ∈ Grp
30 23 11 grpinvf ⊢ G ∈ Grp → inv g ⁡ G : Base G ⟶ Base G
31 29 30 syl ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → inv g ⁡ G : Base G ⟶ Base G
32 31 feqmptd ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → inv g ⁡ G = x ∈ Base G ⟼ inv g ⁡ G ⁡ x
33 22 11 tgpinv ⊢ G ∈ TopGrp → inv g ⁡ G ∈ TopOpen ⁡ G Cn TopOpen ⁡ G
34 33 adantr ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → inv g ⁡ G ∈ TopOpen ⁡ G Cn TopOpen ⁡ G
35 32 34 eqeltrrd ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → x ∈ Base G ⟼ inv g ⁡ G ⁡ x ∈ TopOpen ⁡ G Cn TopOpen ⁡ G
36 21 25 27 35 cnmpt1res ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → x ∈ S ⟼ inv g ⁡ G ⁡ x ∈ TopOpen ⁡ G ↾ 𝑡 S Cn TopOpen ⁡ G
37 20 36 eqeltrd ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → inv g ⁡ H ∈ TopOpen ⁡ G ↾ 𝑡 S Cn TopOpen ⁡ G
38 18 frnd ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → ran ⁡ inv g ⁡ H ⊆ Base H
39 38 9 sseqtrrd ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → ran ⁡ inv g ⁡ H ⊆ S
40 cnrest2 ⊢ TopOpen ⁡ G ∈ TopOn ⁡ Base G ∧ ran ⁡ inv g ⁡ H ⊆ S ∧ S ⊆ Base G → inv g ⁡ H ∈ TopOpen ⁡ G ↾ 𝑡 S Cn TopOpen ⁡ G ↔ inv g ⁡ H ∈ TopOpen ⁡ G ↾ 𝑡 S Cn TopOpen ⁡ G ↾ 𝑡 S
41 25 39 27 40 syl3anc ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → inv g ⁡ H ∈ TopOpen ⁡ G ↾ 𝑡 S Cn TopOpen ⁡ G ↔ inv g ⁡ H ∈ TopOpen ⁡ G ↾ 𝑡 S Cn TopOpen ⁡ G ↾ 𝑡 S
42 37 41 mpbid ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → inv g ⁡ H ∈ TopOpen ⁡ G ↾ 𝑡 S Cn TopOpen ⁡ G ↾ 𝑡 S
43 1 22 resstopn ⊢ TopOpen ⁡ G ↾ 𝑡 S = TopOpen ⁡ H
44 43 12 istgp ⊢ H ∈ TopGrp ↔ H ∈ Grp ∧ H ∈ TopMnd ∧ inv g ⁡ H ∈ TopOpen ⁡ G ↾ 𝑡 S Cn TopOpen ⁡ G ↾ 𝑡 S
45 3 7 42 44 syl3anbrc ⊢ G ∈ TopGrp ∧ S ∈ SubGrp ⁡ G → H ∈ TopGrp