Definition df-slmd 29754

Description: Define the class of all (left) modules over semirings, i.e. semimodules, which are generalizations of left modules. A semimodule is a commutative monoid (=vectors) together with a semiring (=scalars) and a left scalar product connecting them. ( 0 [,] +oo ) for example is not a full fledged left module, but is a semimodule. Definition of [Golan] p. 149. (Contributed by Thierry Arnoux, 21-Mar-2018.)

Assertion

Ref

Expression

df-slmd

|- SLMod = { g e. CMnd | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) }

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

Detailed syntax breakdown of Definition df-slmd

Step	Hyp	Ref	Expression
1		cslmd 29753	. 2 class SLMod
2		vf	. . . . . . . . . . . . 13 setvar f
3	2	cv 1482	. . . . . . . . . . . 12 class f
4		csrg 18505	. . . . . . . . . . . 12 class SRing
5	3, 4	wcel 1990	. . . . . . . . . . 11 wff f e. SRing
6		vr	. . . . . . . . . . . . . . . . . . . 20 setvar r
7	6	cv 1482	. . . . . . . . . . . . . . . . . . 19 class r
8		vw	. . . . . . . . . . . . . . . . . . . 20 setvar w
9	8	cv 1482	. . . . . . . . . . . . . . . . . . 19 class w
10		vs	. . . . . . . . . . . . . . . . . . . 20 setvar s
11	10	cv 1482	. . . . . . . . . . . . . . . . . . 19 class s
12	7, 9, 11	co 6650	. . . . . . . . . . . . . . . . . 18 class ( r s w )
13		vv	. . . . . . . . . . . . . . . . . . 19 setvar v
14	13	cv 1482	. . . . . . . . . . . . . . . . . 18 class v
15	12, 14	wcel 1990	. . . . . . . . . . . . . . . . 17 wff ( r s w ) e. v
16		vx	. . . . . . . . . . . . . . . . . . . . 21 setvar x
17	16	cv 1482	. . . . . . . . . . . . . . . . . . . 20 class x
18		va	. . . . . . . . . . . . . . . . . . . . 21 setvar a
19	18	cv 1482	. . . . . . . . . . . . . . . . . . . 20 class a
20	9, 17, 19	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( w a x )
21	7, 20, 11	co 6650	. . . . . . . . . . . . . . . . . 18 class ( r s ( w a x ) )
22	7, 17, 11	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( r s x )
23	12, 22, 19	co 6650	. . . . . . . . . . . . . . . . . 18 class ( ( r s w ) a ( r s x ) )
24	21, 23	wceq 1483	. . . . . . . . . . . . . . . . 17 wff ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) )
25		vq	. . . . . . . . . . . . . . . . . . . . 21 setvar q
26	25	cv 1482	. . . . . . . . . . . . . . . . . . . 20 class q
27		vp	. . . . . . . . . . . . . . . . . . . . 21 setvar p
28	27	cv 1482	. . . . . . . . . . . . . . . . . . . 20 class p
29	26, 7, 28	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( q p r )
30	29, 9, 11	co 6650	. . . . . . . . . . . . . . . . . 18 class ( ( q p r ) s w )
31	26, 9, 11	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( q s w )
32	31, 12, 19	co 6650	. . . . . . . . . . . . . . . . . 18 class ( ( q s w ) a ( r s w ) )
33	30, 32	wceq 1483	. . . . . . . . . . . . . . . . 17 wff ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) )
34	15, 24, 33	w3a 1037	. . . . . . . . . . . . . . . 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 1482	. . . . . . . . . . . . . . . . . . . 20 class t
37	26, 7, 36	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( q t r )
38	37, 9, 11	co 6650	. . . . . . . . . . . . . . . . . 18 class ( ( q t r ) s w )
39	26, 12, 11	co 6650	. . . . . . . . . . . . . . . . . 18 class ( q s ( r s w ) )
40	38, 39	wceq 1483	. . . . . . . . . . . . . . . . 17 wff ( ( q t r ) s w ) = ( q s ( r s w ) )
41		cur 18501	. . . . . . . . . . . . . . . . . . . 20 class 1r
42	3, 41	cfv 5888	. . . . . . . . . . . . . . . . . . 19 class ( 1r ` f )
43	42, 9, 11	co 6650	. . . . . . . . . . . . . . . . . 18 class ( ( 1r ` f ) s w )
44	43, 9	wceq 1483	. . . . . . . . . . . . . . . . 17 wff ( ( 1r ` f ) s w ) = w
45		c0g 16100	. . . . . . . . . . . . . . . . . . . 20 class 0g
46	3, 45	cfv 5888	. . . . . . . . . . . . . . . . . . 19 class ( 0g ` f )
47	46, 9, 11	co 6650	. . . . . . . . . . . . . . . . . 18 class ( ( 0g ` f ) s w )
48		vg	. . . . . . . . . . . . . . . . . . . 20 setvar g
49	48	cv 1482	. . . . . . . . . . . . . . . . . . 19 class g
50	49, 45	cfv 5888	. . . . . . . . . . . . . . . . . 18 class ( 0g ` g )
51	47, 50	wceq 1483	. . . . . . . . . . . . . . . . 17 wff ( ( 0g ` f ) s w ) = ( 0g ` g )
52	40, 44, 51	w3a 1037	. . . . . . . . . . . . . . . 16 wff ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) )
53	34, 52	wa 384	. . . . . . . . . . . . . . 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) )
54	53, 8, 14	wral 2912	. . . . . . . . . . . . . 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) )
55	54, 16, 14	wral 2912	. . . . . . . . . . . . 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) )
56		vk	. . . . . . . . . . . . . 14 setvar k
57	56	cv 1482	. . . . . . . . . . . . 13 class k
58	55, 6, 57	wral 2912	. . . . . . . . . . . 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) )
59	58, 25, 57	wral 2912	. . . . . . . . . . 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) )
60	5, 59	wa 384	. . . . . . . . . 10 wff ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) )
61		cmulr 15942	. . . . . . . . . . 11 class .r
62	3, 61	cfv 5888	. . . . . . . . . 10 class ( .r ` f )
63	60, 35, 62	wsbc 3435	. . . . . . . . 9 wff [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) )
64		cplusg 15941	. . . . . . . . . 10 class +g
65	3, 64	cfv 5888	. . . . . . . . 9 class ( +g ` f )
66	63, 27, 65	wsbc 3435	. . . . . . . 8 wff [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) )
67		cbs 15857	. . . . . . . . 9 class Base
68	3, 67	cfv 5888	. . . . . . . 8 class ( Base ` f )
69	66, 56, 68	wsbc 3435	. . . . . . 7 wff [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) )
70		csca 15944	. . . . . . . 8 class Scalar
71	49, 70	cfv 5888	. . . . . . 7 class (Scalar ` g )
72	69, 2, 71	wsbc 3435	. . . . . 6 wff [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) )
73		cvsca 15945	. . . . . . 7 class .s
74	49, 73	cfv 5888	. . . . . 6 class ( .s ` g )
75	72, 10, 74	wsbc 3435	. . . . 5 wff [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) )
76	49, 64	cfv 5888	. . . . 5 class ( +g ` g )
77	75, 18, 76	wsbc 3435	. . . 4 wff [. ( +g ` g ) / a ]. [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) )
78	49, 67	cfv 5888	. . . 4 class ( Base ` g )
79	77, 13, 78	wsbc 3435	. . 3 wff [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) )
80		ccmn 18193	. . 3 class CMnd
81	79, 48, 80	crab 2916	. 2 class { g e. CMnd | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) }
82	1, 81	wceq 1483	1 wff SLMod = { g e. CMnd | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. ( .s ` g ) / s ]. [. (Scalar ` g ) / f ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. SRing /\ 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 /\ ( ( 0g ` f ) s w ) = ( 0g ` g ) ) ) ) }

This definition is referenced by:  isslmd  29755