Metamath Proof Explorer

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 ⊢LMod=g∈Grp|[˙Baseg/v]˙[˙+g/a]˙[˙Scalar⁡g/f]˙[˙⋅g/s]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmod classLMod
1 vg setvarg
2 cgrp classGrp
3 cbs classBase
4 1 cv setvarg
5 4 3 cfv classBaseg
6 vv setvarv
7 cplusg class+𝑔
8 4 7 cfv class+g
9 va setvara
10 csca classScalar
11 4 10 cfv classScalar⁡g
12 vf setvarf
13 cvsca class⋅𝑠
14 4 13 cfv class⋅g
15 vs setvars
16 12 cv setvarf
17 16 3 cfv classBasef
18 vk setvark
19 16 7 cfv class+f
20 vp setvarp
21 cmulr class⋅𝑟
22 16 21 cfv class⋅f
23 vt setvart
24 crg classRing
25 16 24 wcel wfff∈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 classrsw
36 35 30 wcel wffrsw∈v
37 9 cv setvara
38 29 cv setvarx
39 34 38 37 co classwax
40 32 39 33 co classrswax
41 32 38 33 co classrsx
42 35 41 37 co classrswarsx
43 40 42 wceq wffrswax=rswarsx
44 26 cv setvarq
45 20 cv setvarp
46 44 32 45 co classqpr
47 46 34 33 co classqprsw
48 44 34 33 co classqsw
49 48 35 37 co classqswarsw
50 47 49 wceq wffqprsw=qswarsw
51 36 43 50 w3a wffrsw∈v∧rswax=rswarsx∧qprsw=qswarsw
52 23 cv setvart
53 44 32 52 co classqtr
54 53 34 33 co classqtrsw
55 44 35 33 co classqsrsw
56 54 55 wceq wffqtrsw=qsrsw
57 cur class1r
58 16 57 cfv class1f
59 58 34 33 co class1fsw
60 59 34 wceq wff1fsw=w
61 56 60 wa wffqtrsw=qsrsw∧1fsw=w
62 51 61 wa wffrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
63 62 31 30 wral wff∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
64 63 29 30 wral wff∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
65 64 28 27 wral wff∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
66 65 26 27 wral wff∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
67 25 66 wa wfff∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
68 67 23 22 wsbc wff[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
69 68 20 19 wsbc wff[˙+f/p]˙[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
70 69 18 17 wsbc wff[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
71 70 15 14 wsbc wff[˙⋅g/s]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
72 71 12 11 wsbc wff[˙Scalar⁡g/f]˙[˙⋅g/s]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
73 72 9 8 wsbc wff[˙+g/a]˙[˙Scalar⁡g/f]˙[˙⋅g/s]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
74 73 6 5 wsbc wff[˙Baseg/v]˙[˙+g/a]˙[˙Scalar⁡g/f]˙[˙⋅g/s]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
75 74 1 2 crab classg∈Grp|[˙Baseg/v]˙[˙+g/a]˙[˙Scalar⁡g/f]˙[˙⋅g/s]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w
76 0 75 wceq wffLMod=g∈Grp|[˙Baseg/v]˙[˙+g/a]˙[˙Scalar⁡g/f]˙[˙⋅g/s]˙[˙Basef/k]˙[˙+f/p]˙[˙⋅f/t]˙f∈Ring∧∀q∈k∀r∈k∀x∈v∀w∈vrsw∈v∧rswax=rswarsx∧qprsw=qswarsw∧qtrsw=qsrsw∧1fsw=w