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 )