Definition df-clm 22863

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 18784), left modules over such subrings are the same as right modules, see rmodislmod 18931. Therefore, we drop the word "left" from "subcomplex left module". (Contributed by Mario Carneiro, 16-Oct-2015.)

Assertion

Ref	Expression
df-clm	|- CMod = { w e. LMod | [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ k e. (SubRing ` ℂfld ) ) }

Distinct variable group:   f, k, w

Detailed syntax breakdown of Definition df-clm

Step	Hyp	Ref	Expression
1		cclm 22862	. 2 class CMod
2		vf	. . . . . . . 8 setvar f
3	2	cv 1482	. . . . . . 7 class f
4		ccnfld 19746	. . . . . . . 8 class ℂfld
5		vk	. . . . . . . . 9 setvar k
6	5	cv 1482	. . . . . . . 8 class k
7		cress 15858	. . . . . . . 8 class ↾s
8	4, 6, 7	co 6650	. . . . . . 7 class (ℂfld ↾s k )
9	3, 8	wceq 1483	. . . . . 6 wff f = (ℂfld ↾s k )
10		csubrg 18776	. . . . . . . 8 class SubRing
11	4, 10	cfv 5888	. . . . . . 7 class (SubRing ` ℂfld )
12	6, 11	wcel 1990	. . . . . 6 wff k e. (SubRing ` ℂfld )
13	9, 12	wa 384	. . . . 5 wff ( f = (ℂfld ↾s k ) /\ k e. (SubRing ` ℂfld ) )
14		cbs 15857	. . . . . 6 class Base
15	3, 14	cfv 5888	. . . . 5 class ( Base ` f )
16	13, 5, 15	wsbc 3435	. . . 4 wff [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ k e. (SubRing ` ℂfld ) )
17		vw	. . . . . 6 setvar w
18	17	cv 1482	. . . . 5 class w
19		csca 15944	. . . . 5 class Scalar
20	18, 19	cfv 5888	. . . 4 class (Scalar ` w )
21	16, 2, 20	wsbc 3435	. . 3 wff [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ k e. (SubRing ` ℂfld ) )
22		clmod 18863	. . 3 class LMod
23	21, 17, 22	crab 2916	. 2 class { w e. LMod | [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ k e. (SubRing ` ℂfld ) ) }
24	1, 23	wceq 1483	1 wff CMod = { w e. LMod | [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ k e. (SubRing ` ℂfld ) ) }

This definition is referenced by:  isclm  22864