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	|- T = ( CCfld toNrmGrp abs )
Assertion	cnindmet	|- ( dist ` T ) = ( abs o. - )

Proof

Step	Hyp	Ref	Expression
1		cnindmet.t	|- T = ( CCfld toNrmGrp abs )
2		absabv	|- abs e. ( AbsVal ` CCfld )
3		cnfldsub	|- - = ( -g ` CCfld )
4	1 3	tngds	|- ( abs e. ( AbsVal ` CCfld ) -> ( abs o. - ) = ( dist ` T ) )
5	2 4	ax-mp	|- ( abs o. - ) = ( dist ` T )
6	5	eqcomi	|- ( dist ` T ) = ( abs o. - )