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 ⊢ H = G ↾ 𝑠 S
Assertion submtmd ⊢ G ∈ TopMnd ∧ S ∈ SubMnd ⁡ G → H ∈ TopMnd

Proof

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