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	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
Assertion	cnncvs	⊢ 𝐶 ∈ ( NrmVec ∩ ℂVec )

Proof

Step	Hyp	Ref	Expression
1		cnrnvc.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
2	1	cnrnvc	⊢ 𝐶 ∈ NrmVec
3	1	cncvs	⊢ 𝐶 ∈ ℂVec
4	2 3	elini	⊢ 𝐶 ∈ ( NrmVec ∩ ℂVec )