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 25096
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 20575), left modules over such subrings are the same as right modules, see rmodislmod 20928. 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 25095 . 2 class ℂMod
2 vf . . . . . . . 8 setvar 𝑓
32cv 1539 . . . . . . 7 class 𝑓
4 ccnfld 21364 . . . . . . . 8 class fld
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1539 . . . . . . . 8 class 𝑘
7 cress 17274 . . . . . . . 8 class s
84, 6, 7co 7431 . . . . . . 7 class (ℂflds 𝑘)
93, 8wceq 1540 . . . . . 6 wff 𝑓 = (ℂflds 𝑘)
10 csubrg 20569 . . . . . . . 8 class SubRing
114, 10cfv 6561 . . . . . . 7 class (SubRing‘ℂfld)
126, 11wcel 2108 . . . . . 6 wff 𝑘 ∈ (SubRing‘ℂfld)
139, 12wa 395 . . . . 5 wff (𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
14 cbs 17247 . . . . . 6 class Base
153, 14cfv 6561 . . . . 5 class (Base‘𝑓)
1613, 5, 15wsbc 3788 . . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
17 vw . . . . . 6 setvar 𝑤
1817cv 1539 . . . . 5 class 𝑤
19 csca 17300 . . . . 5 class Scalar
2018, 19cfv 6561 . . . 4 class (Scalar‘𝑤)
2116, 2, 20wsbc 3788 . . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
22 clmod 20858 . . 3 class LMod
2321, 17, 22crab 3436 . 2 class {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
241, 23wceq 1540 1 wff ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
Colors of variables: wff setvar class
This definition is referenced by:  isclm  25097
  Copyright terms: Public domain W3C validator