# Metamath Proof Explorer

## 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)=ℂ×ℂ$
10 8 9 ax-mp ${⊢}\bigcup \mathrm{metUnif}\left(\mathrm{abs}\circ -\right)=ℂ×ℂ$
11 10 eqcomi ${⊢}ℂ×ℂ=\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 ${⊢}ℂ×ℂ=\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)$