Metamath Proof Explorer


Definition df-clm

Description: Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers CCfld , which allows us to use the complex addition, multiplication, etc. in theorems about subcomplex modules. Since the field of complex numbers is commutative and so are its subrings (see subrgcrng ), left modules over such subrings are the same as right modules, see rmodislmod . Therefore, we drop the word "left" from "subcomplex left module". (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Assertion df-clm CMod=wLMod|[˙Scalarw/f]˙[˙Basef/k]˙f=fld𝑠kkSubRingfld

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclm classCMod
1 vw setvarw
2 clmod classLMod
3 csca classScalar
4 1 cv setvarw
5 4 3 cfv classScalarw
6 vf setvarf
7 cbs classBase
8 6 cv setvarf
9 8 7 cfv classBasef
10 vk setvark
11 ccnfld classfld
12 cress class𝑠
13 10 cv setvark
14 11 13 12 co classfld𝑠k
15 8 14 wceq wfff=fld𝑠k
16 csubrg classSubRing
17 11 16 cfv classSubRingfld
18 13 17 wcel wffkSubRingfld
19 15 18 wa wfff=fld𝑠kkSubRingfld
20 19 10 9 wsbc wff[˙Basef/k]˙f=fld𝑠kkSubRingfld
21 20 6 5 wsbc wff[˙Scalarw/f]˙[˙Basef/k]˙f=fld𝑠kkSubRingfld
22 21 1 2 crab classwLMod|[˙Scalarw/f]˙[˙Basef/k]˙f=fld𝑠kkSubRingfld
23 0 22 wceq wffCMod=wLMod|[˙Scalarw/f]˙[˙Basef/k]˙f=fld𝑠kkSubRingfld