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 22602
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 ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
Distinct variable group:   𝑓,𝑘,𝑤

Detailed syntax breakdown of Definition df-clm
StepHypRef Expression
1 cclm 22601 . 2 class ℂMod
2 vf . . . . . . . 8 setvar 𝑓
32cv 1473 . . . . . . 7 class 𝑓
4 ccnfld 19513 . . . . . . . 8 class fld
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1473 . . . . . . . 8 class 𝑘
7 cress 15642 . . . . . . . 8 class s
84, 6, 7co 6527 . . . . . . 7 class (ℂflds 𝑘)
93, 8wceq 1474 . . . . . 6 wff 𝑓 = (ℂflds 𝑘)
10 csubrg 18545 . . . . . . . 8 class SubRing
114, 10cfv 5790 . . . . . . 7 class (SubRing‘ℂfld)
126, 11wcel 1976 . . . . . 6 wff 𝑘 ∈ (SubRing‘ℂfld)
139, 12wa 382 . . . . 5 wff (𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
14 cbs 15641 . . . . . 6 class Base
153, 14cfv 5790 . . . . 5 class (Base‘𝑓)
1613, 5, 15wsbc 3401 . . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
17 vw . . . . . 6 setvar 𝑤
1817cv 1473 . . . . 5 class 𝑤
19 csca 15717 . . . . 5 class Scalar
2018, 19cfv 5790 . . . 4 class (Scalar‘𝑤)
2116, 2, 20wsbc 3401 . . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
22 clmod 18632 . . 3 class LMod
2321, 17, 22crab 2899 . 2 class {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
241, 23wceq 1474 1 wff ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
Colors of variables: wff setvar class
This definition is referenced by:  isclm  22603
  Copyright terms: Public domain W3C validator