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 22909
Description: Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers fld, 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 18832), left modules over such subrings are the same as right modules, see rmodislmod 18979. 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 22908 . 2 class ℂMod
2 vf . . . . . . . 8 setvar 𝑓
32cv 1522 . . . . . . 7 class 𝑓
4 ccnfld 19794 . . . . . . . 8 class fld
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1522 . . . . . . . 8 class 𝑘
7 cress 15905 . . . . . . . 8 class s
84, 6, 7co 6690 . . . . . . 7 class (ℂflds 𝑘)
93, 8wceq 1523 . . . . . 6 wff 𝑓 = (ℂflds 𝑘)
10 csubrg 18824 . . . . . . . 8 class SubRing
114, 10cfv 5926 . . . . . . 7 class (SubRing‘ℂfld)
126, 11wcel 2030 . . . . . 6 wff 𝑘 ∈ (SubRing‘ℂfld)
139, 12wa 383 . . . . 5 wff (𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
14 cbs 15904 . . . . . 6 class Base
153, 14cfv 5926 . . . . 5 class (Base‘𝑓)
1613, 5, 15wsbc 3468 . . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
17 vw . . . . . 6 setvar 𝑤
1817cv 1522 . . . . 5 class 𝑤
19 csca 15991 . . . . 5 class Scalar
2018, 19cfv 5926 . . . 4 class (Scalar‘𝑤)
2116, 2, 20wsbc 3468 . . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
22 clmod 18911 . . 3 class LMod
2321, 17, 22crab 2945 . 2 class {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
241, 23wceq 1523 1 wff ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
Colors of variables: wff setvar class
This definition is referenced by:  isclm  22910
  Copyright terms: Public domain W3C validator