Definition df-clm 25273

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 20724), left modules over such subrings are the same as right modules, see rmodislmod 21101. 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 25272	. 2 class ℂMod
2		vf	. . . . . . . 8 setvar 𝑓
3	2	cv 1569	. . . . . . 7 class 𝑓
4		ccnfld 21572	. . . . . . . 8 class ℂfld
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1569	. . . . . . . 8 class 𝑘
7		cress 17312	. . . . . . . 8 class ↾s
8	4, 6, 7	co 7419	. . . . . . 7 class (ℂfld ↾s 𝑘)
9	3, 8	wceq 1570	. . . . . 6 wff 𝑓 = (ℂfld ↾s 𝑘)
10		csubrg 20718	. . . . . . . 8 class SubRing
11	4, 10	cfv 6540	. . . . . . 7 class (SubRing‘ℂfld)
12	6, 11	wcel 2146	. . . . . 6 wff 𝑘 ∈ (SubRing‘ℂfld)
13	9, 12	wa 401	. . . . 5 wff (𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
14		cbs 17291	. . . . . 6 class Base
15	3, 14	cfv 6540	. . . . 5 class (Base‘𝑓)
16	13, 5, 15	wsbc 3746	. . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
17		vw	. . . . . 6 setvar 𝑤
18	17	cv 1569	. . . . 5 class 𝑤
19		csca 17335	. . . . 5 class Scalar
20	18, 19	cfv 6540	. . . 4 class (Scalar‘𝑤)
21	16, 2, 20	wsbc 3746	. . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
22		clmod 21031	. . 3 class LMod
23	21, 17, 22	crab 3418	. 2 class {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
24	1, 23	wceq 1570	1 wff ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}

This definition is used by:  isclm  25274