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=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cnncvs	$$⊢C\in \left(\mathrm{NrmVec}\cap \mathrm{ℂVec}\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnrnvc.c	$$⊢C=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	cnrnvc	$$⊢C\in \mathrm{NrmVec}$$
3	1	cncvs	$$⊢C\in \mathrm{ℂVec}$$
4	2 3	elini	$$⊢C\in \left(\mathrm{NrmVec}\cap \mathrm{ℂVec}\right)$$