This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑈 = ( UnifSt ‘ ℂfld )
Assertion cnflduss 𝑈 = ( metUnif ‘ ( abs ∘ − ) )

Proof

Step Hyp Ref Expression
1 cnflduss.1 ⊢ 𝑈 = ( UnifSt ‘ ℂfld )
2 0cn ⊢ 0 ∈ ℂ
3 2 ne0ii ⊢ ℂ ≠ ∅
4 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
5 xmetpsmet ⊢ ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → ( abs ∘ − ) ∈ ( PsMet ‘ ℂ ) )
6 4 5 ax-mp ⊢ ( abs ∘ − ) ∈ ( PsMet ‘ ℂ )
7 metuust ⊢ ( ( ℂ ≠ ∅ ∧ ( abs ∘ − ) ∈ ( PsMet ‘ ℂ ) ) → ( metUnif ‘ ( abs ∘ − ) ) ∈ ( UnifOn ‘ ℂ ) )
8 3 6 7 mp2an ⊢ ( metUnif ‘ ( abs ∘ − ) ) ∈ ( UnifOn ‘ ℂ )
9 ustuni ⊢ ( ( metUnif ‘ ( abs ∘ − ) ) ∈ ( UnifOn ‘ ℂ ) → ∪ ( metUnif ‘ ( abs ∘ − ) ) = ( ℂ × ℂ ) )
10 8 9 ax-mp ⊢ ∪ ( metUnif ‘ ( abs ∘ − ) ) = ( ℂ × ℂ )
11 10 eqcomi ⊢ ( ℂ × ℂ ) = ∪ ( metUnif ‘ ( abs ∘ − ) )
12 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
13 cnfldunif ⊢ ( metUnif ‘ ( abs ∘ − ) ) = ( UnifSet ‘ ℂfld )
14 12 13 ussid ⊢ ( ( ℂ × ℂ ) = ∪ ( metUnif ‘ ( abs ∘ − ) ) → ( metUnif ‘ ( abs ∘ − ) ) = ( UnifSt ‘ ℂfld ) )
15 11 14 ax-mp ⊢ ( metUnif ‘ ( abs ∘ − ) ) = ( UnifSt ‘ ℂfld )
16 1 15 eqtr4i ⊢ 𝑈 = ( metUnif ‘ ( abs ∘ − ) )