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 ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
Assertion subgtgp ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ TopGrp )

Proof

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