Theorem cnindmet

Description: The metric induced on the complex numbers. cnmet proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds and also cnmet . (Contributed by Steve Rodriguez, 5-Dec-2006) (Revised by AV, 17-Oct-2021)

	Ref	Expression
Hypothesis	cnindmet.t	⊢ 𝑇 = ( ℂfld toNrmGrp abs )
Assertion	cnindmet	⊢ ( dist ‘ 𝑇 ) = ( abs ∘ − )

Proof

Step	Hyp	Ref	Expression
1		cnindmet.t	⊢ 𝑇 = ( ℂfld toNrmGrp abs )
2		absabv	⊢ abs ∈ ( AbsVal ‘ ℂfld )
3		cnfldsub	⊢ − = ( -g ‘ ℂfld )
4	1 3	tngds	⊢ ( abs ∈ ( AbsVal ‘ ℂfld ) → ( abs ∘ − ) = ( dist ‘ 𝑇 ) )
5	2 4	ax-mp	⊢ ( abs ∘ − ) = ( dist ‘ 𝑇 )
6	5	eqcomi	⊢ ( dist ‘ 𝑇 ) = ( abs ∘ − )