Definition df-clm 23231

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 19139), left modules over such subrings are the same as right modules, see rmodislmod 19286. 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‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}

Distinct variable group:   𝑓,𝑘,𝑤

Detailed syntax breakdown of Definition df-clm

Step	Hyp	Ref	Expression
1		cclm 23230	. 2 class ℂMod
2		vf	. . . . . . . 8 setvar 𝑓
3	2	cv 1657	. . . . . . 7 class 𝑓
4		ccnfld 20105	. . . . . . . 8 class ℂfld
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1657	. . . . . . . 8 class 𝑘
7		cress 16222	. . . . . . . 8 class ↾s
8	4, 6, 7	co 6904	. . . . . . 7 class (ℂfld ↾s 𝑘)
9	3, 8	wceq 1658	. . . . . 6 wff 𝑓 = (ℂfld ↾s 𝑘)
10		csubrg 19131	. . . . . . . 8 class SubRing
11	4, 10	cfv 6122	. . . . . . 7 class (SubRing‘ℂfld)
12	6, 11	wcel 2166	. . . . . 6 wff 𝑘 ∈ (SubRing‘ℂfld)
13	9, 12	wa 386	. . . . 5 wff (𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
14		cbs 16221	. . . . . 6 class Base
15	3, 14	cfv 6122	. . . . 5 class (Base‘𝑓)
16	13, 5, 15	wsbc 3661	. . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
17		vw	. . . . . 6 setvar 𝑤
18	17	cv 1657	. . . . 5 class 𝑤
19		csca 16307	. . . . 5 class Scalar
20	18, 19	cfv 6122	. . . 4 class (Scalar‘𝑤)
21	16, 2, 20	wsbc 3661	. . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
22		clmod 19218	. . 3 class LMod
23	21, 17, 22	crab 3120	. 2 class {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
24	1, 23	wceq 1658	1 wff ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}

This definition is referenced by:  isclm  23232