Metamath Proof Explorer


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 C = ringLMod fld
Assertion cncvs C ℂVec

Proof

Step Hyp Ref Expression
1 cnrlmod.c C = ringLMod fld
2 1 cnrlmod C LMod
3 cnfldex fld V
4 cnfldbas = Base fld
5 4 ressid fld V fld 𝑠 = fld
6 3 5 ax-mp fld 𝑠 = fld
7 6 eqcomi fld = fld 𝑠
8 id x x
9 addcl x y x + y
10 negcl x x
11 ax-1cn 1
12 mulcl x y x y
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 = C
17 16 fveq2i Scalar ringLMod fld = Scalar C
18 15 17 eqtri fld = Scalar C
19 18 isclmi C LMod fld = fld 𝑠 SubRing fld C CMod
20 2 7 13 19 mp3an C CMod
21 1 cnrlvec C LVec
22 20 21 elini C CMod LVec
23 df-cvs ℂVec = CMod LVec
24 22 23 eleqtrri C ℂVec