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 ⊢ 𝐹 ∈ ( 𝑆 MndHom 𝑇 )
mhmhmeotmd.h ⊢ 𝐹 ∈ ( ( TopOpen ‘ 𝑆 ) Homeo ( TopOpen ‘ 𝑇 ) )
mhmhmeotmd.t ⊢ 𝑆 ∈ TopMnd
mhmhmeotmd.s ⊢ 𝑇 ∈ TopSp
Assertion mhmhmeotmd 𝑇 ∈ TopMnd

Proof

Step Hyp Ref Expression
1 mhmhmeotmd.m ⊢ 𝐹 ∈ ( 𝑆 MndHom 𝑇 )
2 mhmhmeotmd.h ⊢ 𝐹 ∈ ( ( TopOpen ‘ 𝑆 ) Homeo ( TopOpen ‘ 𝑇 ) )
3 mhmhmeotmd.t ⊢ 𝑆 ∈ TopMnd
4 mhmhmeotmd.s ⊢ 𝑇 ∈ TopSp
5 mhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑇 ∈ Mnd )
6 1 5 ax-mp ⊢ 𝑇 ∈ Mnd
7 mhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑆 ∈ Mnd )
8 1 7 ax-mp ⊢ 𝑆 ∈ Mnd
9 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10 eqid ⊢ ( +𝑓 ‘ 𝑆 ) = ( +𝑓 ‘ 𝑆 )
11 9 10 mndplusf ⊢ ( 𝑆 ∈ Mnd → ( +𝑓 ‘ 𝑆 ) : ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ⟶ ( Base ‘ 𝑆 ) )
12 8 11 ax-mp ⊢ ( +𝑓 ‘ 𝑆 ) : ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) ⟶ ( Base ‘ 𝑆 )
13 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
14 eqid ⊢ ( +𝑓 ‘ 𝑇 ) = ( +𝑓 ‘ 𝑇 )
15 13 14 mndplusf ⊢ ( 𝑇 ∈ Mnd → ( +𝑓 ‘ 𝑇 ) : ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ⟶ ( Base ‘ 𝑇 ) )
16 6 15 ax-mp ⊢ ( +𝑓 ‘ 𝑇 ) : ( ( Base ‘ 𝑇 ) × ( Base ‘ 𝑇 ) ) ⟶ ( Base ‘ 𝑇 )
17 eqid ⊢ ( TopOpen ‘ 𝑆 ) = ( TopOpen ‘ 𝑆 )
18 17 9 tmdtopon ⊢ ( 𝑆 ∈ TopMnd → ( TopOpen ‘ 𝑆 ) ∈ ( TopOn ‘ ( Base ‘ 𝑆 ) ) )
19 3 18 ax-mp ⊢ ( TopOpen ‘ 𝑆 ) ∈ ( TopOn ‘ ( Base ‘ 𝑆 ) )
20 eqid ⊢ ( TopOpen ‘ 𝑇 ) = ( TopOpen ‘ 𝑇 )
21 13 20 istps ⊢ ( 𝑇 ∈ TopSp ↔ ( TopOpen ‘ 𝑇 ) ∈ ( TopOn ‘ ( Base ‘ 𝑇 ) ) )
22 4 21 mpbi ⊢ ( TopOpen ‘ 𝑇 ) ∈ ( TopOn ‘ ( Base ‘ 𝑇 ) )
23 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
24 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
25 9 23 24 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
26 1 25 mp3an1 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
27 9 23 10 plusfval ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +𝑓 ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
28 27 fveq2d ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +𝑓 ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
29 9 13 mhmf ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
30 1 29 ax-mp ⊢ 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 )
31 30 ffvelcdmi ⊢ ( 𝑥 ∈ ( Base ‘ 𝑆 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
32 30 ffvelcdmi ⊢ ( 𝑦 ∈ ( Base ‘ 𝑆 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑇 ) )
33 13 24 14 plusfval ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +𝑓 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
34 31 32 33 syl2an ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +𝑓 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
35 26 28 34 3eqtr4d ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +𝑓 ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +𝑓 ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
36 17 10 tmdcn ⊢ ( 𝑆 ∈ TopMnd → ( +𝑓 ‘ 𝑆 ) ∈ ( ( ( TopOpen ‘ 𝑆 ) ×t ( TopOpen ‘ 𝑆 ) ) Cn ( TopOpen ‘ 𝑆 ) ) )
37 3 36 ax-mp ⊢ ( +𝑓 ‘ 𝑆 ) ∈ ( ( ( TopOpen ‘ 𝑆 ) ×t ( TopOpen ‘ 𝑆 ) ) Cn ( TopOpen ‘ 𝑆 ) )
38 2 12 16 19 22 35 37 mndpluscn ⊢ ( +𝑓 ‘ 𝑇 ) ∈ ( ( ( TopOpen ‘ 𝑇 ) ×t ( TopOpen ‘ 𝑇 ) ) Cn ( TopOpen ‘ 𝑇 ) )
39 14 20 istmd ⊢ ( 𝑇 ∈ TopMnd ↔ ( 𝑇 ∈ Mnd ∧ 𝑇 ∈ TopSp ∧ ( +𝑓 ‘ 𝑇 ) ∈ ( ( ( TopOpen ‘ 𝑇 ) ×t ( TopOpen ‘ 𝑇 ) ) Cn ( TopOpen ‘ 𝑇 ) ) ) )
40 6 4 38 39 mpbir3an ⊢ 𝑇 ∈ TopMnd