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

Proof

Step	Hyp	Ref	Expression
1		cnrnvc.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
2		cnnrg	⊢ ℂfld ∈ NrmRing
3		cndrng	⊢ ℂfld ∈ DivRing
4		rlmnvc	⊢ ( ( ℂfld ∈ NrmRing ∧ ℂfld ∈ DivRing ) → ( ringLMod ‘ ℂfld ) ∈ NrmVec )
5	1 4	eqeltrid	⊢ ( ( ℂfld ∈ NrmRing ∧ ℂfld ∈ DivRing ) → 𝐶 ∈ NrmVec )
6	2 3 5	mp2an	⊢ 𝐶 ∈ NrmVec