Theorem cnflduss

Description: The uniform structure of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

	Ref	Expression
Hypothesis	cnflduss.1	$$⊢U=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cnflduss	$$⊢U=\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnflduss.1	$$⊢U=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)$$
2		0cn	$$⊢0\in ℂ$$
3	2	ne0ii	$$⊢ℂ\ne \varnothing$$
4		cnxmet	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$$
5		xmetpsmet	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\to \mathrm{abs}\circ -\in \mathrm{PsMet}\left(ℂ\right)$$
6	4 5	ax-mp	$$⊢\mathrm{abs}\circ -\in \mathrm{PsMet}\left(ℂ\right)$$
7		metuust	$$⊢\left(ℂ\ne \varnothing \wedge \mathrm{abs}\circ -\in \mathrm{PsMet}\left(ℂ\right)\right)\to \mathrm{metUnif}\left(\mathrm{abs}\circ -\right)\in \mathrm{UnifOn}\left(ℂ\right)$$
8	3 6 7	mp2an	$$⊢\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)\in \mathrm{UnifOn}\left(ℂ\right)$$
9		ustuni	$$⊢\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)\in \mathrm{UnifOn}\left(ℂ\right)\to \bigcup \mathrm{metUnif}\left(\mathrm{abs}\circ -\right)=ℂ\times ℂ$$
10	8 9	ax-mp	$$⊢\bigcup \mathrm{metUnif}\left(\mathrm{abs}\circ -\right)=ℂ\times ℂ$$
11	10	eqcomi	$$⊢ℂ\times ℂ=\bigcup \mathrm{metUnif}\left(\mathrm{abs}\circ -\right)$$
12		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
13		cnfldunif	$$⊢\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)=\mathrm{UnifSet}\left({ℂ}_{\mathrm{fld}}\right)$$
14	12 13	ussid	$$⊢ℂ\times ℂ=\bigcup \mathrm{metUnif}\left(\mathrm{abs}\circ -\right)\to \mathrm{metUnif}\left(\mathrm{abs}\circ -\right)=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)$$
15	11 14	ax-mp	$$⊢\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}\right)$$
16	1 15	eqtr4i	$$⊢U=\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)$$