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 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 ), 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	⊢ ℂMod = { 𝑤 ∈ LMod ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclm	⊢ ℂMod
1		vw	⊢ 𝑤
2		clmod	⊢ LMod
3		csca	⊢ Scalar
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( Scalar ‘ 𝑤 )
6		vf	⊢ 𝑓
7		cbs	⊢ Base
8	6	cv	⊢ 𝑓
9	8 7	cfv	⊢ ( Base ‘ 𝑓 )
10		vk	⊢ 𝑘
11		ccnfld	⊢ ℂfld
12		cress	⊢ ↾s
13	10	cv	⊢ 𝑘
14	11 13 12	co	⊢ ( ℂfld ↾s 𝑘 )
15	8 14	wceq	⊢ 𝑓 = ( ℂfld ↾s 𝑘 )
16		csubrg	⊢ SubRing
17	11 16	cfv	⊢ ( SubRing ‘ ℂfld )
18	13 17	wcel	⊢ 𝑘 ∈ ( SubRing ‘ ℂfld )
19	15 18	wa	⊢ ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) )
20	19 10 9	wsbc	⊢ [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) )
21	20 6 5	wsbc	⊢ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) )
22	21 1 2	crab	⊢ { 𝑤 ∈ LMod ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) }
23	0 22	wceq	⊢ ℂMod = { 𝑤 ∈ LMod ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) }