MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clm Unicode version

Definition df-clm 18561
Description: Define a complex module, which is just a left module over a subring of  CC, which allows us to use conventional addition, multiplication, etc. in the left module theorems. (Contributed by Mario Carneiro, 16-Oct-2015.)
Assertion
Ref Expression
df-clm  |- CMod  =  {
w  e.  LMod  |  [. (Scalar `  w )  / 
f ]. [. ( Base `  f )  /  k ]. ( f  =  (flds  k )  /\  k  e.  (SubRing ` fld ) ) }
Distinct variable group:    f, k, w

Detailed syntax breakdown of Definition df-clm
StepHypRef Expression
1 cclm 18560 . 2  class CMod
2 vf . . . . . . . 8  set  f
32cv 1622 . . . . . . 7  class  f
4 ccnfld 16377 . . . . . . . 8  classfld
5 vk . . . . . . . . 9  set  k
65cv 1622 . . . . . . . 8  class  k
7 cress 13149 . . . . . . . 8  classs
84, 6, 7co 5858 . . . . . . 7  class  (flds  k )
93, 8wceq 1623 . . . . . 6  wff  f  =  (flds  k )
10 csubrg 15541 . . . . . . . 8  class SubRing
114, 10cfv 5255 . . . . . . 7  class  (SubRing ` fld )
126, 11wcel 1684 . . . . . 6  wff  k  e.  (SubRing ` fld )
139, 12wa 358 . . . . 5  wff  ( f  =  (flds  k )  /\  k  e.  (SubRing ` fld ) )
14 cbs 13148 . . . . . 6  class  Base
153, 14cfv 5255 . . . . 5  class  ( Base `  f )
1613, 5, 15wsbc 2991 . . . 4  wff  [. ( Base `  f )  / 
k ]. ( f  =  (flds  k )  /\  k  e.  (SubRing ` fld ) )
17 vw . . . . . 6  set  w
1817cv 1622 . . . . 5  class  w
19 csca 13211 . . . . 5  class Scalar
2018, 19cfv 5255 . . . 4  class  (Scalar `  w )
2116, 2, 20wsbc 2991 . . 3  wff  [. (Scalar `  w )  /  f ]. [. ( Base `  f
)  /  k ]. ( f  =  (flds  k )  /\  k  e.  (SubRing ` fld ) )
22 clmod 15627 . . 3  class  LMod
2321, 17, 22crab 2547 . 2  class  { w  e.  LMod  |  [. (Scalar `  w )  /  f ]. [. ( Base `  f
)  /  k ]. ( f  =  (flds  k )  /\  k  e.  (SubRing ` fld ) ) }
241, 23wceq 1623 1  wff CMod  =  {
w  e.  LMod  |  [. (Scalar `  w )  / 
f ]. [. ( Base `  f )  /  k ]. ( f  =  (flds  k )  /\  k  e.  (SubRing ` fld ) ) }
Colors of variables: wff set class
This definition is referenced by:  isclm  18562
  Copyright terms: Public domain W3C validator