Theorem cnncvs

Description: The module of complex numbers (as a module over itself) is a normed subcomplex vector space. The vector operation is + , the scalar product is x. , and the norm is abs (see cnnm ) . (Contributed by Steve Rodriguez, 3-Dec-2006) (Revised by AV, 9-Oct-2021)

	Ref	Expression
Hypothesis	cnrnvc.c	|- C = ( ringLMod ` CCfld )
Assertion	cnncvs	|- C e. ( NrmVec i^i CVec )

Proof

Step	Hyp	Ref	Expression
1		cnrnvc.c	|- C = ( ringLMod ` CCfld )
2	1	cnrnvc	|- C e. NrmVec
3	1	cncvs	|- C e. CVec
4	2 3	elini	|- C e. ( NrmVec i^i CVec )