Definition df-lmod 13845

Description: Define the class of all left modules, which are generalizations of left vector spaces. A left module over a ring is an (Abelian) group (vectors) together with a ring (scalars) and a left scalar product connecting them. (Contributed by NM, 4-Nov-2013.)

Assertion

Ref

Expression

df-lmod

|- LMod = { g e. Grp | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. (Scalar ` g ) / f ]. [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) ) }

Distinct variable group:   f, a, g, k, p, q, r, s, t, v, w, x

Detailed syntax breakdown of Definition df-lmod

Step	Hyp	Ref	Expression
1		clmod 13843	. 2 class LMod
2		vf	. . . . . . . . . . . . 13 setvar f
3	2	cv 1363	. . . . . . . . . . . 12 class f
4		crg 13552	. . . . . . . . . . . 12 class Ring
5	3, 4	wcel 2167	. . . . . . . . . . 11 wff f e. Ring
6		vr	. . . . . . . . . . . . . . . . . . . 20 setvar r
7	6	cv 1363	. . . . . . . . . . . . . . . . . . 19 class r
8		vw	. . . . . . . . . . . . . . . . . . . 20 setvar w
9	8	cv 1363	. . . . . . . . . . . . . . . . . . 19 class w
10		vs	. . . . . . . . . . . . . . . . . . . 20 setvar s
11	10	cv 1363	. . . . . . . . . . . . . . . . . . 19 class s
12	7, 9, 11	co 5922	. . . . . . . . . . . . . . . . . 18 class ( r s w )
13		vv	. . . . . . . . . . . . . . . . . . 19 setvar v
14	13	cv 1363	. . . . . . . . . . . . . . . . . 18 class v
15	12, 14	wcel 2167	. . . . . . . . . . . . . . . . 17 wff ( r s w ) e. v
16		vx	. . . . . . . . . . . . . . . . . . . . 21 setvar x
17	16	cv 1363	. . . . . . . . . . . . . . . . . . . 20 class x
18		va	. . . . . . . . . . . . . . . . . . . . 21 setvar a
19	18	cv 1363	. . . . . . . . . . . . . . . . . . . 20 class a
20	9, 17, 19	co 5922	. . . . . . . . . . . . . . . . . . 19 class ( w a x )
21	7, 20, 11	co 5922	. . . . . . . . . . . . . . . . . 18 class ( r s ( w a x ) )
22	7, 17, 11	co 5922	. . . . . . . . . . . . . . . . . . 19 class ( r s x )
23	12, 22, 19	co 5922	. . . . . . . . . . . . . . . . . 18 class ( ( r s w ) a ( r s x ) )
24	21, 23	wceq 1364	. . . . . . . . . . . . . . . . 17 wff ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) )
25		vq	. . . . . . . . . . . . . . . . . . . . 21 setvar q
26	25	cv 1363	. . . . . . . . . . . . . . . . . . . 20 class q
27		vp	. . . . . . . . . . . . . . . . . . . . 21 setvar p
28	27	cv 1363	. . . . . . . . . . . . . . . . . . . 20 class p
29	26, 7, 28	co 5922	. . . . . . . . . . . . . . . . . . 19 class ( q p r )
30	29, 9, 11	co 5922	. . . . . . . . . . . . . . . . . 18 class ( ( q p r ) s w )
31	26, 9, 11	co 5922	. . . . . . . . . . . . . . . . . . 19 class ( q s w )
32	31, 12, 19	co 5922	. . . . . . . . . . . . . . . . . 18 class ( ( q s w ) a ( r s w ) )
33	30, 32	wceq 1364	. . . . . . . . . . . . . . . . 17 wff ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) )
34	15, 24, 33	w3a 980	. . . . . . . . . . . . . . . 16 wff ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) )
35		vt	. . . . . . . . . . . . . . . . . . . . 21 setvar t
36	35	cv 1363	. . . . . . . . . . . . . . . . . . . 20 class t
37	26, 7, 36	co 5922	. . . . . . . . . . . . . . . . . . 19 class ( q t r )
38	37, 9, 11	co 5922	. . . . . . . . . . . . . . . . . 18 class ( ( q t r ) s w )
39	26, 12, 11	co 5922	. . . . . . . . . . . . . . . . . 18 class ( q s ( r s w ) )
40	38, 39	wceq 1364	. . . . . . . . . . . . . . . . 17 wff ( ( q t r ) s w ) = ( q s ( r s w ) )
41		cur 13515	. . . . . . . . . . . . . . . . . . . 20 class 1r
42	3, 41	cfv 5258	. . . . . . . . . . . . . . . . . . 19 class ( 1r ` f )
43	42, 9, 11	co 5922	. . . . . . . . . . . . . . . . . 18 class ( ( 1r ` f ) s w )
44	43, 9	wceq 1364	. . . . . . . . . . . . . . . . 17 wff ( ( 1r ` f ) s w ) = w
45	40, 44	wa 104	. . . . . . . . . . . . . . . 16 wff ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w )
46	34, 45	wa 104	. . . . . . . . . . . . . . 15 wff ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) )
47	46, 8, 14	wral 2475	. . . . . . . . . . . . . 14 wff A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) )
48	47, 16, 14	wral 2475	. . . . . . . . . . . . 13 wff A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) )
49		vk	. . . . . . . . . . . . . 14 setvar k
50	49	cv 1363	. . . . . . . . . . . . 13 class k
51	48, 6, 50	wral 2475	. . . . . . . . . . . 12 wff A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) )
52	51, 25, 50	wral 2475	. . . . . . . . . . 11 wff A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) )
53	5, 52	wa 104	. . . . . . . . . 10 wff ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) )
54		cmulr 12756	. . . . . . . . . . 11 class .r
55	3, 54	cfv 5258	. . . . . . . . . 10 class ( .r ` f )
56	53, 35, 55	wsbc 2989	. . . . . . . . 9 wff [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) )
57		cplusg 12755	. . . . . . . . . 10 class +g
58	3, 57	cfv 5258	. . . . . . . . 9 class ( +g ` f )
59	56, 27, 58	wsbc 2989	. . . . . . . 8 wff [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) )
60		cbs 12678	. . . . . . . . 9 class Base
61	3, 60	cfv 5258	. . . . . . . 8 class ( Base ` f )
62	59, 49, 61	wsbc 2989	. . . . . . 7 wff [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) )
63		vg	. . . . . . . . 9 setvar g
64	63	cv 1363	. . . . . . . 8 class g
65		cvsca 12759	. . . . . . . 8 class .s
66	64, 65	cfv 5258	. . . . . . 7 class ( .s ` g )
67	62, 10, 66	wsbc 2989	. . . . . 6 wff [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) )
68		csca 12758	. . . . . . 7 class Scalar
69	64, 68	cfv 5258	. . . . . 6 class (Scalar ` g )
70	67, 2, 69	wsbc 2989	. . . . 5 wff [. (Scalar ` g ) / f ]. [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) )
71	64, 57	cfv 5258	. . . . 5 class ( +g ` g )
72	70, 18, 71	wsbc 2989	. . . 4 wff [. ( +g ` g ) / a ]. [. (Scalar ` g ) / f ]. [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) )
73	64, 60	cfv 5258	. . . 4 class ( Base ` g )
74	72, 13, 73	wsbc 2989	. . 3 wff [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. (Scalar ` g ) / f ]. [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) )
75		cgrp 13132	. . 3 class Grp
76	74, 63, 75	crab 2479	. 2 class { g e. Grp | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. (Scalar ` g ) / f ]. [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) ) }
77	1, 76	wceq 1364	1 wff LMod = { g e. Grp | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. (Scalar ` g ) / f ]. [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) ) }

This definition is referenced by:  islmod  13847