Metamath Proof Explorer


Theorem mhmhmeotmd

Description: Deduce a Topological Monoid using mapping that is both a homeomorphism and a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017)

Ref Expression
Hypotheses mhmhmeotmd.m
|- F e. ( S MndHom T )
mhmhmeotmd.h
|- F e. ( ( TopOpen ` S ) Homeo ( TopOpen ` T ) )
mhmhmeotmd.t
|- S e. TopMnd
mhmhmeotmd.s
|- T e. TopSp
Assertion mhmhmeotmd
|- T e. TopMnd

Proof

Step Hyp Ref Expression
1 mhmhmeotmd.m
 |-  F e. ( S MndHom T )
2 mhmhmeotmd.h
 |-  F e. ( ( TopOpen ` S ) Homeo ( TopOpen ` T ) )
3 mhmhmeotmd.t
 |-  S e. TopMnd
4 mhmhmeotmd.s
 |-  T e. TopSp
5 mhmrcl2
 |-  ( F e. ( S MndHom T ) -> T e. Mnd )
6 1 5 ax-mp
 |-  T e. Mnd
7 mhmrcl1
 |-  ( F e. ( S MndHom T ) -> S e. Mnd )
8 1 7 ax-mp
 |-  S e. Mnd
9 eqid
 |-  ( Base ` S ) = ( Base ` S )
10 eqid
 |-  ( +f ` S ) = ( +f ` S )
11 9 10 mndplusf
 |-  ( S e. Mnd -> ( +f ` S ) : ( ( Base ` S ) X. ( Base ` S ) ) --> ( Base ` S ) )
12 8 11 ax-mp
 |-  ( +f ` S ) : ( ( Base ` S ) X. ( Base ` S ) ) --> ( Base ` S )
13 eqid
 |-  ( Base ` T ) = ( Base ` T )
14 eqid
 |-  ( +f ` T ) = ( +f ` T )
15 13 14 mndplusf
 |-  ( T e. Mnd -> ( +f ` T ) : ( ( Base ` T ) X. ( Base ` T ) ) --> ( Base ` T ) )
16 6 15 ax-mp
 |-  ( +f ` T ) : ( ( Base ` T ) X. ( Base ` T ) ) --> ( Base ` T )
17 eqid
 |-  ( TopOpen ` S ) = ( TopOpen ` S )
18 17 9 tmdtopon
 |-  ( S e. TopMnd -> ( TopOpen ` S ) e. ( TopOn ` ( Base ` S ) ) )
19 3 18 ax-mp
 |-  ( TopOpen ` S ) e. ( TopOn ` ( Base ` S ) )
20 eqid
 |-  ( TopOpen ` T ) = ( TopOpen ` T )
21 13 20 istps
 |-  ( T e. TopSp <-> ( TopOpen ` T ) e. ( TopOn ` ( Base ` T ) ) )
22 4 21 mpbi
 |-  ( TopOpen ` T ) e. ( TopOn ` ( Base ` T ) )
23 eqid
 |-  ( +g ` S ) = ( +g ` S )
24 eqid
 |-  ( +g ` T ) = ( +g ` T )
25 9 23 24 mhmlin
 |-  ( ( F e. ( S MndHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
26 1 25 mp3an1
 |-  ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
27 9 23 10 plusfval
 |-  ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +f ` S ) y ) = ( x ( +g ` S ) y ) )
28 27 fveq2d
 |-  ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +f ` S ) y ) ) = ( F ` ( x ( +g ` S ) y ) ) )
29 9 13 mhmf
 |-  ( F e. ( S MndHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
30 1 29 ax-mp
 |-  F : ( Base ` S ) --> ( Base ` T )
31 30 ffvelrni
 |-  ( x e. ( Base ` S ) -> ( F ` x ) e. ( Base ` T ) )
32 30 ffvelrni
 |-  ( y e. ( Base ` S ) -> ( F ` y ) e. ( Base ` T ) )
33 13 24 14 plusfval
 |-  ( ( ( F ` x ) e. ( Base ` T ) /\ ( F ` y ) e. ( Base ` T ) ) -> ( ( F ` x ) ( +f ` T ) ( F ` y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
34 31 32 33 syl2an
 |-  ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( ( F ` x ) ( +f ` T ) ( F ` y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
35 26 28 34 3eqtr4d
 |-  ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +f ` S ) y ) ) = ( ( F ` x ) ( +f ` T ) ( F ` y ) ) )
36 17 10 tmdcn
 |-  ( S e. TopMnd -> ( +f ` S ) e. ( ( ( TopOpen ` S ) tX ( TopOpen ` S ) ) Cn ( TopOpen ` S ) ) )
37 3 36 ax-mp
 |-  ( +f ` S ) e. ( ( ( TopOpen ` S ) tX ( TopOpen ` S ) ) Cn ( TopOpen ` S ) )
38 2 12 16 19 22 35 37 mndpluscn
 |-  ( +f ` T ) e. ( ( ( TopOpen ` T ) tX ( TopOpen ` T ) ) Cn ( TopOpen ` T ) )
39 14 20 istmd
 |-  ( T e. TopMnd <-> ( T e. Mnd /\ T e. TopSp /\ ( +f ` T ) e. ( ( ( TopOpen ` T ) tX ( TopOpen ` T ) ) Cn ( TopOpen ` T ) ) ) )
40 6 4 38 39 mpbir3an
 |-  T e. TopMnd