Definition df-clm

Description: Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers CCfld , 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 ), left modules over such subrings are the same as right modules, see rmodislmod . Therefore, we drop the word "left" from "subcomplex left module". (Contributed by Mario Carneiro, 16-Oct-2015)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclm	|- CMod
1		vw	|- w
2		clmod	|- LMod
3		csca	|- Scalar
4	1	cv	|- w
5	4 3	cfv	|- ( Scalar ` w )
6		vf	|- f
7		cbs	|- Base
8	6	cv	|- f
9	8 7	cfv	|- ( Base ` f )
10		vk	|- k
11		ccnfld	|- CCfld
12		cress	|- |`s
13	10	cv	|- k
14	11 13 12	co	|- ( CCfld |`s k )
15	8 14	wceq	|- f = ( CCfld |`s k )
16		csubrg	|- SubRing
17	11 16	cfv	|- ( SubRing ` CCfld )
18	13 17	wcel	|- k e. ( SubRing ` CCfld )
19	15 18	wa	|- ( f = ( CCfld |`s k ) /\ k e. ( SubRing ` CCfld ) )
20	19 10 9	wsbc	|- [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ k e. ( SubRing ` CCfld ) )
21	20 6 5	wsbc	|- [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ k e. ( SubRing ` CCfld ) )
22	21 1 2	crab	|- { w e. LMod | [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ k e. ( SubRing ` CCfld ) ) }
23	0 22	wceq	|- CMod = { w e. LMod | [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ k e. ( SubRing ` CCfld ) ) }