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‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}

Distinct variable group:   𝑓,𝑘,𝑤

Detailed syntax breakdown of Definition df-clm

Step	Hyp	Ref	Expression
1		cclm 22670	. 2 class ℂMod
2		vf	. . . . . . . 8 setvar 𝑓
3	2	cv 1474	. . . . . . 7 class 𝑓
4		ccnfld 19567	. . . . . . . 8 class ℂfld
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1474	. . . . . . . 8 class 𝑘
7		cress 15696	. . . . . . . 8 class ↾s
8	4, 6, 7	co 6549	. . . . . . 7 class (ℂfld ↾s 𝑘)
9	3, 8	wceq 1475	. . . . . 6 wff 𝑓 = (ℂfld ↾s 𝑘)
10		csubrg 18599	. . . . . . . 8 class SubRing
11	4, 10	cfv 5804	. . . . . . 7 class (SubRing‘ℂfld)
12	6, 11	wcel 1977	. . . . . 6 wff 𝑘 ∈ (SubRing‘ℂfld)
13	9, 12	wa 383	. . . . 5 wff (𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
14		cbs 15695	. . . . . 6 class Base
15	3, 14	cfv 5804	. . . . 5 class (Base‘𝑓)
16	13, 5, 15	wsbc 3402	. . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
17		vw	. . . . . 6 setvar 𝑤
18	17	cv 1474	. . . . 5 class 𝑤
19		csca 15771	. . . . 5 class Scalar
20	18, 19	cfv 5804	. . . 4 class (Scalar‘𝑤)
21	16, 2, 20	wsbc 3402	. . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
22		clmod 18686	. . 3 class LMod
23	21, 17, 22	crab 2900	. 2 class {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
24	1, 23	wceq 1475	1 wff ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}

This definition is referenced by:  isclm  22672