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

Definition df-clm 22671
 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 22670 . 2 class ℂMod
2 vf . . . . . . . 8 setvar 𝑓
32cv 1474 . . . . . . 7 class 𝑓
4 ccnfld 19567 . . . . . . . 8 class fld
5 vk . . . . . . . . 9 setvar 𝑘
65cv 1474 . . . . . . . 8 class 𝑘
7 cress 15696 . . . . . . . 8 class s
84, 6, 7co 6549 . . . . . . 7 class (ℂflds 𝑘)
93, 8wceq 1475 . . . . . 6 wff 𝑓 = (ℂflds 𝑘)
10 csubrg 18599 . . . . . . . 8 class SubRing
114, 10cfv 5804 . . . . . . 7 class (SubRing‘ℂfld)
126, 11wcel 1977 . . . . . 6 wff 𝑘 ∈ (SubRing‘ℂfld)
139, 12wa 383 . . . . 5 wff (𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
14 cbs 15695 . . . . . 6 class Base
153, 14cfv 5804 . . . . 5 class (Base‘𝑓)
1613, 5, 15wsbc 3402 . . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
17 vw . . . . . 6 setvar 𝑤
1817cv 1474 . . . . 5 class 𝑤
19 csca 15771 . . . . 5 class Scalar
2018, 19cfv 5804 . . . 4 class (Scalar‘𝑤)
2116, 2, 20wsbc 3402 . . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
22 clmod 18686 . . 3 class LMod
2321, 17, 22crab 2900 . 2 class {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
241, 23wceq 1475 1 wff ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂflds 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
 Colors of variables: wff setvar class This definition is referenced by:  isclm  22672
 Copyright terms: Public domain W3C validator