Definition df-lmod 20040

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

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

Detailed syntax breakdown of Definition df-lmod

Step	Hyp	Ref	Expression
1		clmod 20038	. 2 class LMod
2		vf	. . . . . . . . . . . . 13 setvar 𝑓
3	2	cv 1538	. . . . . . . . . . . 12 class 𝑓
4		crg 19698	. . . . . . . . . . . 12 class Ring
5	3, 4	wcel 2108	. . . . . . . . . . 11 wff 𝑓 ∈ Ring
6		vr	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑟
7	6	cv 1538	. . . . . . . . . . . . . . . . . . 19 class 𝑟
8		vw	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
9	8	cv 1538	. . . . . . . . . . . . . . . . . . 19 class 𝑤
10		vs	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑠
11	10	cv 1538	. . . . . . . . . . . . . . . . . . 19 class 𝑠
12	7, 9, 11	co 7255	. . . . . . . . . . . . . . . . . 18 class (𝑟𝑠𝑤)
13		vv	. . . . . . . . . . . . . . . . . . 19 setvar 𝑣
14	13	cv 1538	. . . . . . . . . . . . . . . . . 18 class 𝑣
15	12, 14	wcel 2108	. . . . . . . . . . . . . . . . 17 wff (𝑟𝑠𝑤) ∈ 𝑣
16		vx	. . . . . . . . . . . . . . . . . . . . 21 setvar 𝑥
17	16	cv 1538	. . . . . . . . . . . . . . . . . . . 20 class 𝑥
18		va	. . . . . . . . . . . . . . . . . . . . 21 setvar 𝑎
19	18	cv 1538	. . . . . . . . . . . . . . . . . . . 20 class 𝑎
20	9, 17, 19	co 7255	. . . . . . . . . . . . . . . . . . 19 class (𝑤𝑎𝑥)
21	7, 20, 11	co 7255	. . . . . . . . . . . . . . . . . 18 class (𝑟𝑠(𝑤𝑎𝑥))
22	7, 17, 11	co 7255	. . . . . . . . . . . . . . . . . . 19 class (𝑟𝑠𝑥)
23	12, 22, 19	co 7255	. . . . . . . . . . . . . . . . . 18 class ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥))
24	21, 23	wceq 1539	. . . . . . . . . . . . . . . . 17 wff (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥))
25		vq	. . . . . . . . . . . . . . . . . . . . 21 setvar 𝑞
26	25	cv 1538	. . . . . . . . . . . . . . . . . . . 20 class 𝑞
27		vp	. . . . . . . . . . . . . . . . . . . . 21 setvar 𝑝
28	27	cv 1538	. . . . . . . . . . . . . . . . . . . 20 class 𝑝
29	26, 7, 28	co 7255	. . . . . . . . . . . . . . . . . . 19 class (𝑞𝑝𝑟)
30	29, 9, 11	co 7255	. . . . . . . . . . . . . . . . . 18 class ((𝑞𝑝𝑟)𝑠𝑤)
31	26, 9, 11	co 7255	. . . . . . . . . . . . . . . . . . 19 class (𝑞𝑠𝑤)
32	31, 12, 19	co 7255	. . . . . . . . . . . . . . . . . 18 class ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))
33	30, 32	wceq 1539	. . . . . . . . . . . . . . . . 17 wff ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))
34	15, 24, 33	w3a 1085	. . . . . . . . . . . . . . . 16 wff ((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)))
35		vt	. . . . . . . . . . . . . . . . . . . . 21 setvar 𝑡
36	35	cv 1538	. . . . . . . . . . . . . . . . . . . 20 class 𝑡
37	26, 7, 36	co 7255	. . . . . . . . . . . . . . . . . . 19 class (𝑞𝑡𝑟)
38	37, 9, 11	co 7255	. . . . . . . . . . . . . . . . . 18 class ((𝑞𝑡𝑟)𝑠𝑤)
39	26, 12, 11	co 7255	. . . . . . . . . . . . . . . . . 18 class (𝑞𝑠(𝑟𝑠𝑤))
40	38, 39	wceq 1539	. . . . . . . . . . . . . . . . 17 wff ((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))
41		cur 19652	. . . . . . . . . . . . . . . . . . . 20 class 1r
42	3, 41	cfv 6418	. . . . . . . . . . . . . . . . . . 19 class (1r‘𝑓)
43	42, 9, 11	co 7255	. . . . . . . . . . . . . . . . . 18 class ((1r‘𝑓)𝑠𝑤)
44	43, 9	wceq 1539	. . . . . . . . . . . . . . . . 17 wff ((1r‘𝑓)𝑠𝑤) = 𝑤
45	40, 44	wa 395	. . . . . . . . . . . . . . . 16 wff (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)
46	34, 45	wa 395	. . . . . . . . . . . . . . 15 wff (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))
47	46, 8, 14	wral 3063	. . . . . . . . . . . . . 14 wff ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))
48	47, 16, 14	wral 3063	. . . . . . . . . . . . 13 wff ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))
49		vk	. . . . . . . . . . . . . 14 setvar 𝑘
50	49	cv 1538	. . . . . . . . . . . . 13 class 𝑘
51	48, 6, 50	wral 3063	. . . . . . . . . . . 12 wff ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))
52	51, 25, 50	wral 3063	. . . . . . . . . . 11 wff ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤))
53	5, 52	wa 395	. . . . . . . . . 10 wff (𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))
54		cmulr 16889	. . . . . . . . . . 11 class .r
55	3, 54	cfv 6418	. . . . . . . . . 10 class (.r‘𝑓)
56	53, 35, 55	wsbc 3711	. . . . . . . . 9 wff [(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))
57		cplusg 16888	. . . . . . . . . 10 class +g
58	3, 57	cfv 6418	. . . . . . . . 9 class (+g‘𝑓)
59	56, 27, 58	wsbc 3711	. . . . . . . 8 wff [(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))
60		cbs 16840	. . . . . . . . 9 class Base
61	3, 60	cfv 6418	. . . . . . . 8 class (Base‘𝑓)
62	59, 49, 61	wsbc 3711	. . . . . . 7 wff [(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))
63		vg	. . . . . . . . 9 setvar 𝑔
64	63	cv 1538	. . . . . . . 8 class 𝑔
65		cvsca 16892	. . . . . . . 8 class ·𝑠
66	64, 65	cfv 6418	. . . . . . 7 class ( ·𝑠 ‘𝑔)
67	62, 10, 66	wsbc 3711	. . . . . 6 wff [( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))
68		csca 16891	. . . . . . 7 class Scalar
69	64, 68	cfv 6418	. . . . . 6 class (Scalar‘𝑔)
70	67, 2, 69	wsbc 3711	. . . . 5 wff [(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))
71	64, 57	cfv 6418	. . . . 5 class (+g‘𝑔)
72	70, 18, 71	wsbc 3711	. . . 4 wff [(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))
73	64, 60	cfv 6418	. . . 4 class (Base‘𝑔)
74	72, 13, 73	wsbc 3711	. . 3 wff [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))
75		cgrp 18492	. . 3 class Grp
76	74, 63, 75	crab 3067	. 2 class {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))}
77	1, 76	wceq 1539	1 wff LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠 ‘𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞 ∈ 𝑘 ∀𝑟 ∈ 𝑘 ∀𝑥 ∈ 𝑣 ∀𝑤 ∈ 𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r‘𝑓)𝑠𝑤) = 𝑤)))}

This definition is referenced by:  islmod  20042