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 S )
Assertion submtmd
|- ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> H e. TopMnd )

Proof

Step Hyp Ref Expression
1 subgtgp.h
 |-  H = ( G |`s S )
2 1 submmnd
 |-  ( S e. ( SubMnd ` G ) -> H e. Mnd )
3 2 adantl
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> H e. Mnd )
4 tmdtps
 |-  ( G e. TopMnd -> G e. TopSp )
5 resstps
 |-  ( ( G e. TopSp /\ S e. ( SubMnd ` G ) ) -> ( G |`s S ) e. TopSp )
6 4 5 sylan
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( G |`s S ) e. TopSp )
7 1 6 eqeltrid
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> H e. TopSp )
8 eqid
 |-  ( Base ` H ) = ( Base ` H )
9 eqid
 |-  ( +g ` H ) = ( +g ` H )
10 eqid
 |-  ( +f ` H ) = ( +f ` H )
11 8 9 10 plusffval
 |-  ( +f ` H ) = ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> ( x ( +g ` H ) y ) )
12 1 submbas
 |-  ( S e. ( SubMnd ` G ) -> S = ( Base ` H ) )
13 12 adantl
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> S = ( Base ` H ) )
14 eqid
 |-  ( +g ` G ) = ( +g ` G )
15 1 14 ressplusg
 |-  ( S e. ( SubMnd ` G ) -> ( +g ` G ) = ( +g ` H ) )
16 15 adantl
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( +g ` G ) = ( +g ` H ) )
17 16 oveqd
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
18 13 13 17 mpoeq123dv
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( x e. S , y e. S |-> ( x ( +g ` G ) y ) ) = ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> ( x ( +g ` H ) y ) ) )
19 11 18 eqtr4id
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( +f ` H ) = ( x e. S , y e. S |-> ( x ( +g ` G ) y ) ) )
20 eqid
 |-  ( ( TopOpen ` G ) |`t S ) = ( ( TopOpen ` G ) |`t S )
21 eqid
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
22 eqid
 |-  ( Base ` G ) = ( Base ` G )
23 21 22 tmdtopon
 |-  ( G e. TopMnd -> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) )
24 23 adantr
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) )
25 22 submss
 |-  ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
26 25 adantl
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> S C_ ( Base ` G ) )
27 eqid
 |-  ( +f ` G ) = ( +f ` G )
28 22 14 27 plusffval
 |-  ( +f ` G ) = ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` G ) y ) )
29 21 27 tmdcn
 |-  ( G e. TopMnd -> ( +f ` G ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) )
30 28 29 eqeltrrid
 |-  ( G e. TopMnd -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` G ) y ) ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) )
31 30 adantr
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` G ) y ) ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) )
32 20 24 26 20 24 26 31 cnmpt2res
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( x e. S , y e. S |-> ( x ( +g ` G ) y ) ) e. ( ( ( ( TopOpen ` G ) |`t S ) tX ( ( TopOpen ` G ) |`t S ) ) Cn ( TopOpen ` G ) ) )
33 19 32 eqeltrd
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( +f ` H ) e. ( ( ( ( TopOpen ` G ) |`t S ) tX ( ( TopOpen ` G ) |`t S ) ) Cn ( TopOpen ` G ) ) )
34 8 10 mndplusf
 |-  ( H e. Mnd -> ( +f ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) )
35 frn
 |-  ( ( +f ` H ) : ( ( Base ` H ) X. ( Base ` H ) ) --> ( Base ` H ) -> ran ( +f ` H ) C_ ( Base ` H ) )
36 3 34 35 3syl
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ran ( +f ` H ) C_ ( Base ` H ) )
37 36 13 sseqtrrd
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ran ( +f ` H ) C_ S )
38 cnrest2
 |-  ( ( ( TopOpen ` G ) e. ( TopOn ` ( Base ` G ) ) /\ ran ( +f ` H ) C_ S /\ S C_ ( Base ` G ) ) -> ( ( +f ` H ) e. ( ( ( ( TopOpen ` G ) |`t S ) tX ( ( TopOpen ` G ) |`t S ) ) Cn ( TopOpen ` G ) ) <-> ( +f ` H ) e. ( ( ( ( TopOpen ` G ) |`t S ) tX ( ( TopOpen ` G ) |`t S ) ) Cn ( ( TopOpen ` G ) |`t S ) ) ) )
39 24 37 26 38 syl3anc
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( ( +f ` H ) e. ( ( ( ( TopOpen ` G ) |`t S ) tX ( ( TopOpen ` G ) |`t S ) ) Cn ( TopOpen ` G ) ) <-> ( +f ` H ) e. ( ( ( ( TopOpen ` G ) |`t S ) tX ( ( TopOpen ` G ) |`t S ) ) Cn ( ( TopOpen ` G ) |`t S ) ) ) )
40 33 39 mpbid
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> ( +f ` H ) e. ( ( ( ( TopOpen ` G ) |`t S ) tX ( ( TopOpen ` G ) |`t S ) ) Cn ( ( TopOpen ` G ) |`t S ) ) )
41 1 21 resstopn
 |-  ( ( TopOpen ` G ) |`t S ) = ( TopOpen ` H )
42 10 41 istmd
 |-  ( H e. TopMnd <-> ( H e. Mnd /\ H e. TopSp /\ ( +f ` H ) e. ( ( ( ( TopOpen ` G ) |`t S ) tX ( ( TopOpen ` G ) |`t S ) ) Cn ( ( TopOpen ` G ) |`t S ) ) ) )
43 3 7 40 42 syl3anbrc
 |-  ( ( G e. TopMnd /\ S e. ( SubMnd ` G ) ) -> H e. TopMnd )