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\in \left(S\mathrm{MndHom}T\right)$$
	mhmhmeotmd.h	$$⊢F\in \left(\mathrm{TopOpen}\left(S\right)\mathrm{Homeo}\mathrm{TopOpen}\left(T\right)\right)$$
	mhmhmeotmd.t	$$⊢S\in \mathrm{TopMnd}$$
	mhmhmeotmd.s	$$⊢T\in \mathrm{TopSp}$$
Assertion	mhmhmeotmd	$$⊢T\in \mathrm{TopMnd}$$

Proof

Step	Hyp	Ref	Expression
1		mhmhmeotmd.m	$$⊢F\in \left(S\mathrm{MndHom}T\right)$$
2		mhmhmeotmd.h	$$⊢F\in \left(\mathrm{TopOpen}\left(S\right)\mathrm{Homeo}\mathrm{TopOpen}\left(T\right)\right)$$
3		mhmhmeotmd.t	$$⊢S\in \mathrm{TopMnd}$$
4		mhmhmeotmd.s	$$⊢T\in \mathrm{TopSp}$$
5		mhmrcl2	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to T\in \mathrm{Mnd}$$
6	1 5	ax-mp	$$⊢T\in \mathrm{Mnd}$$
7		mhmrcl1	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to S\in \mathrm{Mnd}$$
8	1 7	ax-mp	$$⊢S\in \mathrm{Mnd}$$
9		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
10		eqid	$$⊢{+}_{𝑓}\left(S\right)={+}_{𝑓}\left(S\right)$$
11	9 10	mndplusf	$$⊢S\in \mathrm{Mnd}\to {+}_{𝑓}\left(S\right):{\mathrm{Base}}_S\times {\mathrm{Base}}_S⟶{\mathrm{Base}}_S$$
12	8 11	ax-mp	$$⊢{+}_{𝑓}\left(S\right):{\mathrm{Base}}_S\times {\mathrm{Base}}_S⟶{\mathrm{Base}}_S$$
13		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
14		eqid	$$⊢{+}_{𝑓}\left(T\right)={+}_{𝑓}\left(T\right)$$
15	13 14	mndplusf	$$⊢T\in \mathrm{Mnd}\to {+}_{𝑓}\left(T\right):{\mathrm{Base}}_T\times {\mathrm{Base}}_T⟶{\mathrm{Base}}_T$$
16	6 15	ax-mp	$$⊢{+}_{𝑓}\left(T\right):{\mathrm{Base}}_T\times {\mathrm{Base}}_T⟶{\mathrm{Base}}_T$$
17		eqid	$$⊢\mathrm{TopOpen}\left(S\right)=\mathrm{TopOpen}\left(S\right)$$
18	17 9	tmdtopon	$$⊢S\in \mathrm{TopMnd}\to \mathrm{TopOpen}\left(S\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_S\right)$$
19	3 18	ax-mp	$$⊢\mathrm{TopOpen}\left(S\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_S\right)$$
20		eqid	$$⊢\mathrm{TopOpen}\left(T\right)=\mathrm{TopOpen}\left(T\right)$$
21	13 20	istps	$$⊢T\in \mathrm{TopSp}\leftrightarrow \mathrm{TopOpen}\left(T\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_T\right)$$
22	4 21	mpbi	$$⊢\mathrm{TopOpen}\left(T\right)\in \mathrm{TopOn}\left({\mathrm{Base}}_T\right)$$
23		eqid	$$⊢{+}_S={+}_S$$
24		eqid	$$⊢{+}_T={+}_T$$
25	9 23 24	mhmlin	$$⊢\left(F\in \left(S\mathrm{MndHom}T\right)\wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to F\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)$$
26	1 25	mp3an1	$$⊢\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to F\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)$$
27	9 23 10	plusfval	$$⊢\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x{+}_{𝑓}\left(S\right)y=x{+}_{S}y$$
28	27	fveq2d	$$⊢\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to F\left(x{+}_{𝑓}\left(S\right)y\right)=F\left(x{+}_{S}y\right)$$
29	9 13	mhmf	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to F:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T$$
30	1 29	ax-mp	$$⊢F:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T$$
31	30	ffvelcdmi	$$⊢x\in {\mathrm{Base}}_S\to F\left(x\right)\in {\mathrm{Base}}_T$$
32	30	ffvelcdmi	$$⊢y\in {\mathrm{Base}}_S\to F\left(y\right)\in {\mathrm{Base}}_T$$
33	13 24 14	plusfval	$$⊢\left(F\left(x\right)\in {\mathrm{Base}}_T\wedge F\left(y\right)\in {\mathrm{Base}}_T\right)\to F\left(x\right){+}_{𝑓}\left(T\right)F\left(y\right)=F\left(x\right){+}_{T}F\left(y\right)$$
34	31 32 33	syl2an	$$⊢\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to F\left(x\right){+}_{𝑓}\left(T\right)F\left(y\right)=F\left(x\right){+}_{T}F\left(y\right)$$
35	26 28 34	3eqtr4d	$$⊢\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to F\left(x{+}_{𝑓}\left(S\right)y\right)=F\left(x\right){+}_{𝑓}\left(T\right)F\left(y\right)$$
36	17 10	tmdcn	$$⊢S\in \mathrm{TopMnd}\to {+}_{𝑓}\left(S\right)\in \left(\left(\mathrm{TopOpen}\left(S\right){\times }_t\mathrm{TopOpen}\left(S\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left(S\right)\right)$$
37	3 36	ax-mp	$$⊢{+}_{𝑓}\left(S\right)\in \left(\left(\mathrm{TopOpen}\left(S\right){\times }_t\mathrm{TopOpen}\left(S\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left(S\right)\right)$$
38	2 12 16 19 22 35 37	mndpluscn	$$⊢{+}_{𝑓}\left(T\right)\in \left(\left(\mathrm{TopOpen}\left(T\right){\times }_t\mathrm{TopOpen}\left(T\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left(T\right)\right)$$
39	14 20	istmd	$$⊢T\in \mathrm{TopMnd}\leftrightarrow \left(T\in \mathrm{Mnd}\wedge T\in \mathrm{TopSp}\wedge {+}_{𝑓}\left(T\right)\in \left(\left(\mathrm{TopOpen}\left(T\right){\times }_t\mathrm{TopOpen}\left(T\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left(T\right)\right)\right)$$
40	6 4 38 39	mpbir3an	$$⊢T\in \mathrm{TopMnd}$$