Definition df-lmod

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)

	Ref	Expression
Assertion	df-lmod	$$⊢\mathrm{LMod}=\left\{g\in \mathrm{Grp}|\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmod	$$class\mathrm{LMod}$$
1		vg	$$setvarg$$
2		cgrp	$$class\mathrm{Grp}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarg$$
5	4 3	cfv	$$class{\mathrm{Base}}_g$$
6		vv	$$setvarv$$
7		cplusg	$$class{+}_{𝑔}$$
8	4 7	cfv	$$class{+}_g$$
9		va	$$setvara$$
10		csca	$$class\mathrm{Scalar}$$
11	4 10	cfv	$$class\mathrm{Scalar}\left(g\right)$$
12		vf	$$setvarf$$
13		cvsca	$$class{\cdot }_{𝑠}$$
14	4 13	cfv	$$class{\cdot }_g$$
15		vs	$$setvars$$
16	12	cv	$$setvarf$$
17	16 3	cfv	$$class{\mathrm{Base}}_f$$
18		vk	$$setvark$$
19	16 7	cfv	$$class{+}_f$$
20		vp	$$setvarp$$
21		cmulr	$$class{\cdot }_{𝑟}$$
22	16 21	cfv	$$class{\cdot }_f$$
23		vt	$$setvart$$
24		crg	$$class\mathrm{Ring}$$
25	16 24	wcel	$$wfff\in \mathrm{Ring}$$
26		vq	$$setvarq$$
27	18	cv	$$setvark$$
28		vr	$$setvarr$$
29		vx	$$setvarx$$
30	6	cv	$$setvarv$$
31		vw	$$setvarw$$
32	28	cv	$$setvarr$$
33	15	cv	$$setvars$$
34	31	cv	$$setvarw$$
35	32 34 33	co	$$class\left(rsw\right)$$
36	35 30	wcel	$$wffrsw\in v$$
37	9	cv	$$setvara$$
38	29	cv	$$setvarx$$
39	34 38 37	co	$$class\left(wax\right)$$
40	32 39 33	co	$$class\left(rs\left(wax\right)\right)$$
41	32 38 33	co	$$class\left(rsx\right)$$
42	35 41 37	co	$$class\left(\left(rsw\right)a\left(rsx\right)\right)$$
43	40 42	wceq	$$wffrs\left(wax\right)=\left(rsw\right)a\left(rsx\right)$$
44	26	cv	$$setvarq$$
45	20	cv	$$setvarp$$
46	44 32 45	co	$$class\left(qpr\right)$$
47	46 34 33	co	$$class\left(\left(qpr\right)sw\right)$$
48	44 34 33	co	$$class\left(qsw\right)$$
49	48 35 37	co	$$class\left(\left(qsw\right)a\left(rsw\right)\right)$$
50	47 49	wceq	$$wff\left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)$$
51	36 43 50	w3a	$$wff\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)$$
52	23	cv	$$setvart$$
53	44 32 52	co	$$class\left(qtr\right)$$
54	53 34 33	co	$$class\left(\left(qtr\right)sw\right)$$
55	44 35 33	co	$$class\left(qs\left(rsw\right)\right)$$
56	54 55	wceq	$$wff\left(qtr\right)sw=qs\left(rsw\right)$$
57		cur	$$class{1}_r$$
58	16 57	cfv	$$class{1}_f$$
59	58 34 33	co	$$class\left(1_{f}sw\right)$$
60	59 34	wceq	$$wff{1}_{f}sw=w$$
61	56 60	wa	$$wff\left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)$$
62	51 61	wa	$$wff\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)$$
63	62 31 30	wral	$$wff\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)$$
64	63 29 30	wral	$$wff\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)$$
65	64 28 27	wral	$$wff\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)$$
66	65 26 27	wral	$$wff\forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)$$
67	25 66	wa	$$wff\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
68	67 23 22	wsbc	$$wff\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
69	68 20 19	wsbc	$$wff\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
70	69 18 17	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
71	70 15 14	wsbc	$$wff\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
72	71 12 11	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
73	72 9 8	wsbc	$$wff\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
74	73 6 5	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
75	74 1 2	crab	$$class\left\{g\in \mathrm{Grp}|\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right\}$$
76	0 75	wceq	$$wff\mathrm{LMod}=\left\{g\in \mathrm{Grp}|\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right\}$$