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

Definition df-clm 24977
Description: Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers fld, which allows 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 20503), left modules over such subrings are the same as right modules, see rmodislmod 20802. Therefore, we drop the word "left" from "subcomplex left module". (Contributed by Mario Carneiro, 16-Oct-2015.)
Assertion
Ref Expression
df-clm ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
Distinct variable group:   𝑓,𝑘,𝑤

Detailed syntax breakdown of Definition df-clm
StepHypRef Expression
1 cclm 24976 . 2 class ℂMod
2 vf . . . . . . . 8 setvar 𝑓
32cv 1533 . . . . . . 7 class 𝑓
4 ccnfld 21266 . . . . . . . 8 class fld
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1533 . . . . . . . 8 class 𝑘
7 cress 17200 . . . . . . . 8 class s
84, 6, 7co 7414 . . . . . . 7 class (ℂflds 𝑘)
93, 8wceq 1534 . . . . . 6 wff 𝑓 = (ℂflds 𝑘)
10 csubrg 20495 . . . . . . . 8 class SubRing
114, 10cfv 6542 . . . . . . 7 class (SubRing‘ℂfld)
126, 11wcel 2099 . . . . . 6 wff 𝑘 ∈ (SubRing‘ℂfld)
139, 12wa 395 . . . . 5 wff (𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
14 cbs 17171 . . . . . 6 class Base
153, 14cfv 6542 . . . . 5 class (Base‘𝑓)
1613, 5, 15wsbc 3774 . . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
17 vw . . . . . 6 setvar 𝑤
1817cv 1533 . . . . 5 class 𝑤
19 csca 17227 . . . . 5 class Scalar
2018, 19cfv 6542 . . . 4 class (Scalar‘𝑤)
2116, 2, 20wsbc 3774 . . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
22 clmod 20732 . . 3 class LMod
2321, 17, 22crab 3427 . 2 class {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
241, 23wceq 1534 1 wff ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
Colors of variables: wff setvar class
This definition is referenced by:  isclm  24978
  Copyright terms: Public domain W3C validator