Theorem mndpluscn

Description: A mapping that is both a homeomorphism and a monoid homomorphism preserves the "continuousness" of the operation. (Contributed by Thierry Arnoux, 25-Mar-2017)

	Ref	Expression
Hypotheses	mndpluscn.f	$$⊢F\in \left(J\mathrm{Homeo}K\right)$$
	mndpluscn.p	$$⊢\underset{\dot{}}{+}:B\times B⟶B$$
	mndpluscn.t	$$⊢\underset{\dot{}}{\ast }:C\times C⟶C$$
	mndpluscn.j	$$⊢J\in \mathrm{TopOn}\left(B\right)$$
	mndpluscn.k	$$⊢K\in \mathrm{TopOn}\left(C\right)$$
	mndpluscn.h	$$⊢\left(x\in B\wedge y\in B\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{\ast }F\left(y\right)$$
	mndpluscn.o	$$⊢\underset{\dot{}}{+}\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$
Assertion	mndpluscn	$$⊢\underset{\dot{}}{\ast }\in \left(\left(K{\times }_{t}K\right)\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		mndpluscn.f	$$⊢F\in \left(J\mathrm{Homeo}K\right)$$
2		mndpluscn.p	$$⊢\underset{\dot{}}{+}:B\times B⟶B$$
3		mndpluscn.t	$$⊢\underset{\dot{}}{\ast }:C\times C⟶C$$
4		mndpluscn.j	$$⊢J\in \mathrm{TopOn}\left(B\right)$$
5		mndpluscn.k	$$⊢K\in \mathrm{TopOn}\left(C\right)$$
6		mndpluscn.h	$$⊢\left(x\in B\wedge y\in B\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{\ast }F\left(y\right)$$
7		mndpluscn.o	$$⊢\underset{\dot{}}{+}\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$
8		ffn	$$⊢\underset{\dot{}}{\ast }:C\times C⟶C\to \underset{\dot{}}{\ast }Fn\left(C\times C\right)$$
9		fnov	$$⊢\underset{\dot{}}{\ast }Fn\left(C\times C\right)\leftrightarrow \underset{\dot{}}{\ast }=\left(a\in C,b\in C⟼a\underset{\dot{}}{\ast }b\right)$$
10	9	biimpi	$$⊢\underset{\dot{}}{\ast }Fn\left(C\times C\right)\to \underset{\dot{}}{\ast }=\left(a\in C,b\in C⟼a\underset{\dot{}}{\ast }b\right)$$
11	3 8 10	mp2b	$$⊢\underset{\dot{}}{\ast }=\left(a\in C,b\in C⟼a\underset{\dot{}}{\ast }b\right)$$
12	4	toponunii	$$⊢B=\bigcup J$$
13	5	toponunii	$$⊢C=\bigcup K$$
14	12 13	hmeof1o	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F:B\underset{1-1\; onto}{⟶}C$$
15	1 14	ax-mp	$$⊢F:B\underset{1-1\; onto}{⟶}C$$
16		f1ocnvdm	$$⊢\left(F:B\underset{1-1\; onto}{⟶}C\wedge a\in C\right)\to F^{-1}\left(a\right)\in B$$
17	15 16	mpan	$$⊢a\in C\to F^{-1}\left(a\right)\in B$$
18		f1ocnvdm	$$⊢\left(F:B\underset{1-1\; onto}{⟶}C\wedge b\in C\right)\to F^{-1}\left(b\right)\in B$$
19	15 18	mpan	$$⊢b\in C\to F^{-1}\left(b\right)\in B$$
20	17 19	anim12i	$$⊢\left(a\in C\wedge b\in C\right)\to \left(F^{-1}\left(a\right)\in B\wedge F^{-1}\left(b\right)\in B\right)$$
21	6	rgen2	$$⊢\forall x\in B\forall y\in BF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{\ast }F\left(y\right)$$
22		fvoveq1	$$⊢x=F^{-1}\left(a\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}y\right)$$
23		fveq2	$$⊢x=F^{-1}\left(a\right)\to F\left(x\right)=F\left(F^{-1}\left(a\right)\right)$$
24	23	oveq1d	$$⊢x=F^{-1}\left(a\right)\to F\left(x\right)\underset{\dot{}}{\ast }F\left(y\right)=F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{\ast }F\left(y\right)$$
25	22 24	eqeq12d	$$⊢x=F^{-1}\left(a\right)\to \left(F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{\ast }F\left(y\right)\leftrightarrow F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}y\right)=F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{\ast }F\left(y\right)\right)$$
26		oveq2	$$⊢y=F^{-1}\left(b\right)\to F^{-1}\left(a\right)\underset{\dot{}}{+}y=F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)$$
27	26	fveq2d	$$⊢y=F^{-1}\left(b\right)\to F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}y\right)=F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)$$
28		fveq2	$$⊢y=F^{-1}\left(b\right)\to F\left(y\right)=F\left(F^{-1}\left(b\right)\right)$$
29	28	oveq2d	$$⊢y=F^{-1}\left(b\right)\to F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{\ast }F\left(y\right)=F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{\ast }F\left(F^{-1}\left(b\right)\right)$$
30	27 29	eqeq12d	$$⊢y=F^{-1}\left(b\right)\to \left(F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}y\right)=F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{\ast }F\left(y\right)\leftrightarrow F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)=F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{\ast }F\left(F^{-1}\left(b\right)\right)\right)$$
31	25 30	rspc2va	$$⊢\left(\left(F^{-1}\left(a\right)\in B\wedge F^{-1}\left(b\right)\in B\right)\wedge \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{\ast }F\left(y\right)\right)\to F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)=F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{\ast }F\left(F^{-1}\left(b\right)\right)$$
32	20 21 31	sylancl	$$⊢\left(a\in C\wedge b\in C\right)\to F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)=F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{\ast }F\left(F^{-1}\left(b\right)\right)$$
33		f1ocnvfv2	$$⊢\left(F:B\underset{1-1\; onto}{⟶}C\wedge a\in C\right)\to F\left(F^{-1}\left(a\right)\right)=a$$
34	15 33	mpan	$$⊢a\in C\to F\left(F^{-1}\left(a\right)\right)=a$$
35		f1ocnvfv2	$$⊢\left(F:B\underset{1-1\; onto}{⟶}C\wedge b\in C\right)\to F\left(F^{-1}\left(b\right)\right)=b$$
36	15 35	mpan	$$⊢b\in C\to F\left(F^{-1}\left(b\right)\right)=b$$
37	34 36	oveqan12d	$$⊢\left(a\in C\wedge b\in C\right)\to F\left(F^{-1}\left(a\right)\right)\underset{\dot{}}{\ast }F\left(F^{-1}\left(b\right)\right)=a\underset{\dot{}}{\ast }b$$
38	32 37	eqtr2d	$$⊢\left(a\in C\wedge b\in C\right)\to a\underset{\dot{}}{\ast }b=F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)$$
39	38	mpoeq3ia	$$⊢\left(a\in C,b\in C⟼a\underset{\dot{}}{\ast }b\right)=\left(a\in C,b\in C⟼F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)\right)$$
40	11 39	eqtri	$$⊢\underset{\dot{}}{\ast }=\left(a\in C,b\in C⟼F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)\right)$$
41	5	a1i	$$⊢\top \to K\in \mathrm{TopOn}\left(C\right)$$
42	41 41	cnmpt1st	$$⊢\top \to \left(a\in C,b\in C⟼a\right)\in \left(\left(K{\times }_{t}K\right)\mathrm{Cn}K\right)$$
43		hmeocnvcn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F^{-1}\in \left(K\mathrm{Cn}J\right)$$
44	1 43	mp1i	$$⊢\top \to F^{-1}\in \left(K\mathrm{Cn}J\right)$$
45	41 41 42 44	cnmpt21f	$$⊢\top \to \left(a\in C,b\in C⟼F^{-1}\left(a\right)\right)\in \left(\left(K{\times }_{t}K\right)\mathrm{Cn}J\right)$$
46	41 41	cnmpt2nd	$$⊢\top \to \left(a\in C,b\in C⟼b\right)\in \left(\left(K{\times }_{t}K\right)\mathrm{Cn}K\right)$$
47	41 41 46 44	cnmpt21f	$$⊢\top \to \left(a\in C,b\in C⟼F^{-1}\left(b\right)\right)\in \left(\left(K{\times }_{t}K\right)\mathrm{Cn}J\right)$$
48	7	a1i	$$⊢\top \to \underset{\dot{}}{+}\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$
49	41 41 45 47 48	cnmpt22f	$$⊢\top \to \left(a\in C,b\in C⟼F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)\in \left(\left(K{\times }_{t}K\right)\mathrm{Cn}J\right)$$
50		hmeocn	$$⊢F\in \left(J\mathrm{Homeo}K\right)\to F\in \left(J\mathrm{Cn}K\right)$$
51	1 50	mp1i	$$⊢\top \to F\in \left(J\mathrm{Cn}K\right)$$
52	41 41 49 51	cnmpt21f	$$⊢\top \to \left(a\in C,b\in C⟼F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)\right)\in \left(\left(K{\times }_{t}K\right)\mathrm{Cn}K\right)$$
53	52	mptru	$$⊢\left(a\in C,b\in C⟼F\left(F^{-1}\left(a\right)\underset{\dot{}}{+}{F}^{-1}\left(b\right)\right)\right)\in \left(\left(K{\times }_{t}K\right)\mathrm{Cn}K\right)$$
54	40 53	eqeltri	$$⊢\underset{\dot{}}{\ast }\in \left(\left(K{\times }_{t}K\right)\mathrm{Cn}K\right)$$