Definition df-slmd 32346

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[,]+∞) 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 = {𝑔 ∈ CMnd ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][( ·𝑠 ‘𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤 ∧ ((0g‘𝑓)𝑠𝑤) = (0g‘𝑔))))}

Distinct variable group:   𝑓,𝑎,𝑔,𝑘,𝑝,𝑞,𝑟,𝑠,𝑡,𝑣,𝑤,𝑥

Detailed syntax breakdown of Definition df-slmd

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

This definition is referenced by:  isslmd  32347