Definition df-slmd

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)

	Ref	Expression
Assertion	df-slmd	⊢ SLMod = { 𝑔 ∈ CMnd ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cslmd	⊢ SLMod
1		vg	⊢ 𝑔
2		ccmn	⊢ CMnd
3		cbs	⊢ Base
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( Base ‘ 𝑔 )
6		vv	⊢ 𝑣
7		cplusg	⊢ +g
8	4 7	cfv	⊢ ( +g ‘ 𝑔 )
9		va	⊢ 𝑎
10		cvsca	⊢ ·𝑠
11	4 10	cfv	⊢ ( ·𝑠 ‘ 𝑔 )
12		vs	⊢ 𝑠
13		csca	⊢ Scalar
14	4 13	cfv	⊢ ( Scalar ‘ 𝑔 )
15		vf	⊢ 𝑓
16	15	cv	⊢ 𝑓
17	16 3	cfv	⊢ ( Base ‘ 𝑓 )
18		vk	⊢ 𝑘
19	16 7	cfv	⊢ ( +g ‘ 𝑓 )
20		vp	⊢ 𝑝
21		cmulr	⊢ .r
22	16 21	cfv	⊢ ( .r ‘ 𝑓 )
23		vt	⊢ 𝑡
24		csrg	⊢ SRing
25	16 24	wcel	⊢ 𝑓 ∈ SRing
26		vq	⊢ 𝑞
27	18	cv	⊢ 𝑘
28		vr	⊢ 𝑟
29		vx	⊢ 𝑥
30	6	cv	⊢ 𝑣
31		vw	⊢ 𝑤
32	28	cv	⊢ 𝑟
33	12	cv	⊢ 𝑠
34	31	cv	⊢ 𝑤
35	32 34 33	co	⊢ ( 𝑟 𝑠 𝑤 )
36	35 30	wcel	⊢ ( 𝑟 𝑠 𝑤 ) ∈ 𝑣
37	9	cv	⊢ 𝑎
38	29	cv	⊢ 𝑥
39	34 38 37	co	⊢ ( 𝑤 𝑎 𝑥 )
40	32 39 33	co	⊢ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) )
41	32 38 33	co	⊢ ( 𝑟 𝑠 𝑥 )
42	35 41 37	co	⊢ ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) )
43	40 42	wceq	⊢ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) )
44	26	cv	⊢ 𝑞
45	20	cv	⊢ 𝑝
46	44 32 45	co	⊢ ( 𝑞 𝑝 𝑟 )
47	46 34 33	co	⊢ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 )
48	44 34 33	co	⊢ ( 𝑞 𝑠 𝑤 )
49	48 35 37	co	⊢ ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) )
50	47 49	wceq	⊢ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) )
51	36 43 50	w3a	⊢ ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) )
52	23	cv	⊢ 𝑡
53	44 32 52	co	⊢ ( 𝑞 𝑡 𝑟 )
54	53 34 33	co	⊢ ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 )
55	44 35 33	co	⊢ ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) )
56	54 55	wceq	⊢ ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) )
57		cur	⊢ 1r
58	16 57	cfv	⊢ ( 1r ‘ 𝑓 )
59	58 34 33	co	⊢ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 )
60	59 34	wceq	⊢ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤
61		c0g	⊢ 0g
62	16 61	cfv	⊢ ( 0g ‘ 𝑓 )
63	62 34 33	co	⊢ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 )
64	4 61	cfv	⊢ ( 0g ‘ 𝑔 )
65	63 64	wceq	⊢ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 )
66	56 60 65	w3a	⊢ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) )
67	51 66	wa	⊢ ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) )
68	67 31 30	wral	⊢ ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) )
69	68 29 30	wral	⊢ ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) )
70	69 28 27	wral	⊢ ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) )
71	70 26 27	wral	⊢ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) )
72	25 71	wa	⊢ ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
73	72 23 22	wsbc	⊢ [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
74	73 20 19	wsbc	⊢ [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
75	74 18 17	wsbc	⊢ [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
76	75 15 14	wsbc	⊢ [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
77	76 12 11	wsbc	⊢ [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
78	77 9 8	wsbc	⊢ [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
79	78 6 5	wsbc	⊢ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) )
80	79 1 2	crab	⊢ { 𝑔 ∈ CMnd ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) }
81	0 80	wceq	⊢ SLMod = { 𝑔 ∈ CMnd ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( +g ‘ 𝑔 ) / 𝑎 ] [ ( ·𝑠 ‘ 𝑔 ) / 𝑠 ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ( 𝑓 ∈ SRing ∧ ∀ 𝑞 ∈ 𝑘 ∀ 𝑟 ∈ 𝑘 ∀ 𝑥 ∈ 𝑣 ∀ 𝑤 ∈ 𝑣 ( ( ( 𝑟 𝑠 𝑤 ) ∈ 𝑣 ∧ ( 𝑟 𝑠 ( 𝑤 𝑎 𝑥 ) ) = ( ( 𝑟 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑥 ) ) ∧ ( ( 𝑞 𝑝 𝑟 ) 𝑠 𝑤 ) = ( ( 𝑞 𝑠 𝑤 ) 𝑎 ( 𝑟 𝑠 𝑤 ) ) ) ∧ ( ( ( 𝑞 𝑡 𝑟 ) 𝑠 𝑤 ) = ( 𝑞 𝑠 ( 𝑟 𝑠 𝑤 ) ) ∧ ( ( 1r ‘ 𝑓 ) 𝑠 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ 𝑓 ) 𝑠 𝑤 ) = ( 0g ‘ 𝑔 ) ) ) ) }