Metamath Proof Explorer


Theorem submtmd

Description: A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypothesis subgtgp.h 𝐻 = ( 𝐺s 𝑆 )
Assertion submtmd ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝐻 ∈ TopMnd )

Proof

Step Hyp Ref Expression
1 subgtgp.h 𝐻 = ( 𝐺s 𝑆 )
2 1 submmnd ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐻 ∈ Mnd )
3 2 adantl ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝐻 ∈ Mnd )
4 tmdtps ( 𝐺 ∈ TopMnd → 𝐺 ∈ TopSp )
5 resstps ( ( 𝐺 ∈ TopSp ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝐺s 𝑆 ) ∈ TopSp )
6 4 5 sylan ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝐺s 𝑆 ) ∈ TopSp )
7 1 6 eqeltrid ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝐻 ∈ TopSp )
8 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
9 eqid ( +g𝐻 ) = ( +g𝐻 )
10 eqid ( +𝑓𝐻 ) = ( +𝑓𝐻 )
11 8 9 10 plusffval ( +𝑓𝐻 ) = ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( +g𝐻 ) 𝑦 ) )
12 1 submbas ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
13 12 adantl ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
14 eqid ( +g𝐺 ) = ( +g𝐺 )
15 1 14 ressplusg ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( +g𝐺 ) = ( +g𝐻 ) )
16 15 adantl ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( +g𝐺 ) = ( +g𝐻 ) )
17 16 oveqd ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) = ( 𝑥 ( +g𝐻 ) 𝑦 ) )
18 13 13 17 mpoeq123dv ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑥𝑆 , 𝑦𝑆 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐻 ) , 𝑦 ∈ ( Base ‘ 𝐻 ) ↦ ( 𝑥 ( +g𝐻 ) 𝑦 ) ) )
19 11 18 eqtr4id ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( +𝑓𝐻 ) = ( 𝑥𝑆 , 𝑦𝑆 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) )
20 eqid ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) = ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 )
21 eqid ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
22 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
23 21 22 tmdtopon ( 𝐺 ∈ TopMnd → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
24 23 adantr ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
25 22 submss ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
26 25 adantl ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
27 eqid ( +𝑓𝐺 ) = ( +𝑓𝐺 )
28 22 14 27 plusffval ( +𝑓𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) )
29 21 27 tmdcn ( 𝐺 ∈ TopMnd → ( +𝑓𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
30 28 29 eqeltrrid ( 𝐺 ∈ TopMnd → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
31 30 adantr ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
32 20 24 26 20 24 26 31 cnmpt2res ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( 𝑥𝑆 , 𝑦𝑆 ↦ ( 𝑥 ( +g𝐺 ) 𝑦 ) ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
33 19 32 eqeltrd ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( +𝑓𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
34 8 10 mndplusf ( 𝐻 ∈ Mnd → ( +𝑓𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) )
35 frn ( ( +𝑓𝐻 ) : ( ( Base ‘ 𝐻 ) × ( Base ‘ 𝐻 ) ) ⟶ ( Base ‘ 𝐻 ) → ran ( +𝑓𝐻 ) ⊆ ( Base ‘ 𝐻 ) )
36 3 34 35 3syl ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ran ( +𝑓𝐻 ) ⊆ ( Base ‘ 𝐻 ) )
37 36 13 sseqtrrd ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ran ( +𝑓𝐻 ) ⊆ 𝑆 )
38 cnrest2 ( ( ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ran ( +𝑓𝐻 ) ⊆ 𝑆𝑆 ⊆ ( Base ‘ 𝐺 ) ) → ( ( +𝑓𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ↔ ( +𝑓𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) ) )
39 24 37 26 38 syl3anc ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( ( +𝑓𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ↔ ( +𝑓𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) ) )
40 33 39 mpbid ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → ( +𝑓𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) )
41 1 21 resstopn ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) = ( TopOpen ‘ 𝐻 )
42 10 41 istmd ( 𝐻 ∈ TopMnd ↔ ( 𝐻 ∈ Mnd ∧ 𝐻 ∈ TopSp ∧ ( +𝑓𝐻 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ×t ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) Cn ( ( TopOpen ‘ 𝐺 ) ↾t 𝑆 ) ) ) )
43 3 7 40 42 syl3anbrc ( ( 𝐺 ∈ TopMnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝐻 ∈ TopMnd )