Theorem cncvs

Description: The complex left module of complex numbers is a subcomplex vector space. The vector operation is + , and the scalar product is x. . (Contributed by NM, 5-Nov-2006) (Revised by AV, 21-Sep-2021)

	Ref	Expression
Hypothesis	cnrlmod.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
Assertion	cncvs	⊢ 𝐶 ∈ ℂVec

Proof

Step	Hyp	Ref	Expression
1		cnrlmod.c	⊢ 𝐶 = ( ringLMod ‘ ℂfld )
2	1	cnrlmod	⊢ 𝐶 ∈ LMod
3		cnfldex	⊢ ℂfld ∈ V
4		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
5	4	ressid	⊢ ( ℂfld ∈ V → ( ℂfld ↾s ℂ ) = ℂfld )
6	3 5	ax-mp	⊢ ( ℂfld ↾s ℂ ) = ℂfld
7	6	eqcomi	⊢ ℂfld = ( ℂfld ↾s ℂ )
8		id	⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
9		addcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
10		negcl	⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
11		ax-1cn	⊢ 1 ∈ ℂ
12		mulcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
13	8 9 10 11 12	cnsubrglem	⊢ ℂ ∈ ( SubRing ‘ ℂfld )
14		rlmsca	⊢ ( ℂfld ∈ V → ℂfld = ( Scalar ‘ ( ringLMod ‘ ℂfld ) ) )
15	3 14	ax-mp	⊢ ℂfld = ( Scalar ‘ ( ringLMod ‘ ℂfld ) )
16	1	eqcomi	⊢ ( ringLMod ‘ ℂfld ) = 𝐶
17	16	fveq2i	⊢ ( Scalar ‘ ( ringLMod ‘ ℂfld ) ) = ( Scalar ‘ 𝐶 )
18	15 17	eqtri	⊢ ℂfld = ( Scalar ‘ 𝐶 )
19	18	isclmi	⊢ ( ( 𝐶 ∈ LMod ∧ ℂfld = ( ℂfld ↾s ℂ ) ∧ ℂ ∈ ( SubRing ‘ ℂfld ) ) → 𝐶 ∈ ℂMod )
20	2 7 13 19	mp3an	⊢ 𝐶 ∈ ℂMod
21	1	cnrlvec	⊢ 𝐶 ∈ LVec
22	20 21	elini	⊢ 𝐶 ∈ ( ℂMod ∩ LVec )
23		df-cvs	⊢ ℂVec = ( ℂMod ∩ LVec )
24	22 23	eleqtrri	⊢ 𝐶 ∈ ℂVec