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 ∘ − ) )