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 )