Theorem cnrnvc

Description: The module of complex numbers (as a module over itself) is a normed vector space over itself. The vector operation is + , and the scalar product is x. , and the norm function is abs . (Contributed by AV, 9-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		cnrnvc.c	|- C = ( ringLMod ` CCfld )
2		cnnrg	|- CCfld e. NrmRing
3		cndrng	|- CCfld e. DivRing
4		rlmnvc	|- ( ( CCfld e. NrmRing /\ CCfld e. DivRing ) -> ( ringLMod ` CCfld ) e. NrmVec )
5	1 4	eqeltrid	|- ( ( CCfld e. NrmRing /\ CCfld e. DivRing ) -> C e. NrmVec )
6	2 3 5	mp2an	|- C e. NrmVec