This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ` CCfld )
Assertion cncvs 
|- C e. CVec

Proof

Step Hyp Ref Expression
1 cnrlmod.c 
 |-  C = ( ringLMod ` CCfld )
2 1 cnrlmod 
 |-  C e. LMod
3 cnfldex 
 |-  CCfld e. _V
4 cnfldbas 
 |-  CC = ( Base ` CCfld )
5 4 ressid 
 |-  ( CCfld e. _V -> ( CCfld |`s CC ) = CCfld )
6 3 5 ax-mp 
 |-  ( CCfld |`s CC ) = CCfld
7 6 eqcomi 
 |-  CCfld = ( CCfld |`s CC )
8 id 
 |-  ( x e. CC -> x e. CC )
9 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
10 negcl 
 |-  ( x e. CC -> -u x e. CC )
11 ax-1cn 
 |-  1 e. CC
12 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
13 8 9 10 11 12 cnsubrglem 
 |-  CC e. ( SubRing ` CCfld )
14 rlmsca 
 |-  ( CCfld e. _V -> CCfld = ( Scalar ` ( ringLMod ` CCfld ) ) )
15 3 14 ax-mp 
 |-  CCfld = ( Scalar ` ( ringLMod ` CCfld ) )
16 1 eqcomi 
 |-  ( ringLMod ` CCfld ) = C
17 16 fveq2i 
 |-  ( Scalar ` ( ringLMod ` CCfld ) ) = ( Scalar ` C )
18 15 17 eqtri 
 |-  CCfld = ( Scalar ` C )
19 18 isclmi 
 |-  ( ( C e. LMod /\ CCfld = ( CCfld |`s CC ) /\ CC e. ( SubRing ` CCfld ) ) -> C e. CMod )
20 2 7 13 19 mp3an 
 |-  C e. CMod
21 1 cnrlvec 
 |-  C e. LVec
22 20 21 elini 
 |-  C e. ( CMod i^i LVec )
23 df-cvs 
 |-  CVec = ( CMod i^i LVec )
24 22 23 eleqtrri 
 |-  C e. CVec