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

Definition df-clm 20535
 Description: Define a complex module, which is just a left module over a subring of , 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 Scalar flds SubRingfld
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-clm
StepHypRef Expression
1 cclm 20534 . 2 CMod
2 vf . . . . . . . 8
32cv 1363 . . . . . . 7
4 ccnfld 17718 . . . . . . . 8 fld
5 vk . . . . . . . . 9
65cv 1363 . . . . . . . 8
7 cress 14171 . . . . . . . 8 s
84, 6, 7co 6090 . . . . . . 7 flds
93, 8wceq 1364 . . . . . 6 flds
10 csubrg 16841 . . . . . . . 8 SubRing
114, 10cfv 5415 . . . . . . 7 SubRingfld
126, 11wcel 1761 . . . . . 6 SubRingfld
139, 12wa 369 . . . . 5 flds SubRingfld
14 cbs 14170 . . . . . 6
153, 14cfv 5415 . . . . 5
1613, 5, 15wsbc 3183 . . . 4 flds SubRingfld
17 vw . . . . . 6
1817cv 1363 . . . . 5
19 csca 14237 . . . . 5 Scalar
2018, 19cfv 5415 . . . 4 Scalar
2116, 2, 20wsbc 3183 . . 3 Scalar flds SubRingfld
22 clmod 16928 . . 3
2321, 17, 22crab 2717 . 2 Scalar flds SubRingfld
241, 23wceq 1364 1 CMod Scalar flds SubRingfld
 Colors of variables: wff setvar class This definition is referenced by:  isclm  20536
 Copyright terms: Public domain W3C validator