Theorem cnnm

Description: The norm of the normed subcomplex vector space of complex numbers is the absolute value. (Contributed by NM, 12-Jan-2008) (Revised by AV, 9-Oct-2021)

	Ref	Expression
Hypothesis	cnrnvc.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
Assertion	cnnm	⊢ ( norm ‘ 𝐶 ) = abs

Proof

Step	Hyp	Ref	Expression
1		cnrnvc.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
2		rlmnm	⊢ ( norm ‘ ℂfld ) = ( norm ‘ ( ringLMod ‘ ℂfld ) )
3		cnfldnm	⊢ abs = ( norm ‘ ℂfld )
4	1	fveq2i	⊢ ( norm ‘ 𝐶 ) = ( norm ‘ ( ringLMod ‘ ℂfld ) )
5	2 3 4	3eqtr4ri	⊢ ( norm ‘ 𝐶 ) = abs