Definition df-clm 23668

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 19532), left modules over such subrings are the same as right modules, see rmodislmod 19695. 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 23667	. 2 class ℂMod
2		vf	. . . . . . . 8 setvar 𝑓
3	2	cv 1537	. . . . . . 7 class 𝑓
4		ccnfld 20091	. . . . . . . 8 class ℂfld
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1537	. . . . . . . 8 class 𝑘
7		cress 16476	. . . . . . . 8 class ↾s
8	4, 6, 7	co 7135	. . . . . . 7 class (ℂfld ↾s 𝑘)
9	3, 8	wceq 1538	. . . . . 6 wff 𝑓 = (ℂfld ↾s 𝑘)
10		csubrg 19524	. . . . . . . 8 class SubRing
11	4, 10	cfv 6324	. . . . . . 7 class (SubRing‘ℂfld)
12	6, 11	wcel 2111	. . . . . 6 wff 𝑘 ∈ (SubRing‘ℂfld)
13	9, 12	wa 399	. . . . 5 wff (𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
14		cbs 16475	. . . . . 6 class Base
15	3, 14	cfv 6324	. . . . 5 class (Base‘𝑓)
16	13, 5, 15	wsbc 3720	. . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
17		vw	. . . . . 6 setvar 𝑤
18	17	cv 1537	. . . . 5 class 𝑤
19		csca 16560	. . . . 5 class Scalar
20	18, 19	cfv 6324	. . . 4 class (Scalar‘𝑤)
21	16, 2, 20	wsbc 3720	. . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))
22		clmod 19627	. . 3 class LMod
23	21, 17, 22	crab 3110	. 2 class {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}
24	1, 23	wceq 1538	1 wff ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))}

This definition is referenced by:  isclm  23669