Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-slmd Structured version   Visualization version   GIF version

Definition df-slmd 30757
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
StepHypRef Expression
1 cslmd 30756 . 2 class SLMod
2 vf . . . . . . . . . . . . 13 setvar 𝑓
32cv 1527 . . . . . . . . . . . 12 class 𝑓
4 csrg 19186 . . . . . . . . . . . 12 class SRing
53, 4wcel 2105 . . . . . . . . . . 11 wff 𝑓 ∈ SRing
6 vr . . . . . . . . . . . . . . . . . . . 20 setvar 𝑟
76cv 1527 . . . . . . . . . . . . . . . . . . 19 class 𝑟
8 vw . . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
98cv 1527 . . . . . . . . . . . . . . . . . . 19 class 𝑤
10 vs . . . . . . . . . . . . . . . . . . . 20 setvar 𝑠
1110cv 1527 . . . . . . . . . . . . . . . . . . 19 class 𝑠
127, 9, 11co 7145 . . . . . . . . . . . . . . . . . 18 class (𝑟𝑠𝑤)
13 vv . . . . . . . . . . . . . . . . . . 19 setvar 𝑣
1413cv 1527 . . . . . . . . . . . . . . . . . 18 class 𝑣
1512, 14wcel 2105 . . . . . . . . . . . . . . . . 17 wff (𝑟𝑠𝑤) ∈ 𝑣
16 vx . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑥
1716cv 1527 . . . . . . . . . . . . . . . . . . . 20 class 𝑥
18 va . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑎
1918cv 1527 . . . . . . . . . . . . . . . . . . . 20 class 𝑎
209, 17, 19co 7145 . . . . . . . . . . . . . . . . . . 19 class (𝑤𝑎𝑥)
217, 20, 11co 7145 . . . . . . . . . . . . . . . . . 18 class (𝑟𝑠(𝑤𝑎𝑥))
227, 17, 11co 7145 . . . . . . . . . . . . . . . . . . 19 class (𝑟𝑠𝑥)
2312, 22, 19co 7145 . . . . . . . . . . . . . . . . . 18 class ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥))
2421, 23wceq 1528 . . . . . . . . . . . . . . . . 17 wff (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥))
25 vq . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑞
2625cv 1527 . . . . . . . . . . . . . . . . . . . 20 class 𝑞
27 vp . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑝
2827cv 1527 . . . . . . . . . . . . . . . . . . . 20 class 𝑝
2926, 7, 28co 7145 . . . . . . . . . . . . . . . . . . 19 class (𝑞𝑝𝑟)
3029, 9, 11co 7145 . . . . . . . . . . . . . . . . . 18 class ((𝑞𝑝𝑟)𝑠𝑤)
3126, 9, 11co 7145 . . . . . . . . . . . . . . . . . . 19 class (𝑞𝑠𝑤)
3231, 12, 19co 7145 . . . . . . . . . . . . . . . . . 18 class ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))
3330, 32wceq 1528 . . . . . . . . . . . . . . . . 17 wff ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))
3415, 24, 33w3a 1079 . . . . . . . . . . . . . . . 16 wff ((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)))
35 vt . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑡
3635cv 1527 . . . . . . . . . . . . . . . . . . . 20 class 𝑡
3726, 7, 36co 7145 . . . . . . . . . . . . . . . . . . 19 class (𝑞𝑡𝑟)
3837, 9, 11co 7145 . . . . . . . . . . . . . . . . . 18 class ((𝑞𝑡𝑟)𝑠𝑤)
3926, 12, 11co 7145 . . . . . . . . . . . . . . . . . 18 class (𝑞𝑠(𝑟𝑠𝑤))
4038, 39wceq 1528 . . . . . . . . . . . . . . . . 17 wff ((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))
41 cur 19182 . . . . . . . . . . . . . . . . . . . 20 class 1r
423, 41cfv 6349 . . . . . . . . . . . . . . . . . . 19 class (1r𝑓)
4342, 9, 11co 7145 . . . . . . . . . . . . . . . . . 18 class ((1r𝑓)𝑠𝑤)
4443, 9wceq 1528 . . . . . . . . . . . . . . . . 17 wff ((1r𝑓)𝑠𝑤) = 𝑤
45 c0g 16703 . . . . . . . . . . . . . . . . . . . 20 class 0g
463, 45cfv 6349 . . . . . . . . . . . . . . . . . . 19 class (0g𝑓)
4746, 9, 11co 7145 . . . . . . . . . . . . . . . . . 18 class ((0g𝑓)𝑠𝑤)
48 vg . . . . . . . . . . . . . . . . . . . 20 setvar 𝑔
4948cv 1527 . . . . . . . . . . . . . . . . . . 19 class 𝑔
5049, 45cfv 6349 . . . . . . . . . . . . . . . . . 18 class (0g𝑔)
5147, 50wceq 1528 . . . . . . . . . . . . . . . . 17 wff ((0g𝑓)𝑠𝑤) = (0g𝑔)
5240, 44, 51w3a 1079 . . . . . . . . . . . . . . . 16 wff (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))
5334, 52wa 396 . . . . . . . . . . . . . . 15 wff (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))
5453, 8, 14wral 3138 . . . . . . . . . . . . . 14 wff 𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))
5554, 16, 14wral 3138 . . . . . . . . . . . . 13 wff 𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))
56 vk . . . . . . . . . . . . . 14 setvar 𝑘
5756cv 1527 . . . . . . . . . . . . 13 class 𝑘
5855, 6, 57wral 3138 . . . . . . . . . . . 12 wff 𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))
5958, 25, 57wral 3138 . . . . . . . . . . 11 wff 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔)))
605, 59wa 396 . . . . . . . . . 10 wff (𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
61 cmulr 16556 . . . . . . . . . . 11 class .r
623, 61cfv 6349 . . . . . . . . . 10 class (.r𝑓)
6360, 35, 62wsbc 3771 . . . . . . . . 9 wff [(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
64 cplusg 16555 . . . . . . . . . 10 class +g
653, 64cfv 6349 . . . . . . . . 9 class (+g𝑓)
6663, 27, 65wsbc 3771 . . . . . . . 8 wff [(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
67 cbs 16473 . . . . . . . . 9 class Base
683, 67cfv 6349 . . . . . . . 8 class (Base‘𝑓)
6966, 56, 68wsbc 3771 . . . . . . 7 wff [(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
70 csca 16558 . . . . . . . 8 class Scalar
7149, 70cfv 6349 . . . . . . 7 class (Scalar‘𝑔)
7269, 2, 71wsbc 3771 . . . . . 6 wff [(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
73 cvsca 16559 . . . . . . 7 class ·𝑠
7449, 73cfv 6349 . . . . . 6 class ( ·𝑠𝑔)
7572, 10, 74wsbc 3771 . . . . 5 wff [( ·𝑠𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
7649, 64cfv 6349 . . . . 5 class (+g𝑔)
7775, 18, 76wsbc 3771 . . . 4 wff [(+g𝑔) / 𝑎][( ·𝑠𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
7849, 67cfv 6349 . . . 4 class (Base‘𝑔)
7977, 13, 78wsbc 3771 . . 3 wff [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][( ·𝑠𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))
80 ccmn 18837 . . 3 class CMnd
8179, 48, 80crab 3142 . 2 class {𝑔 ∈ CMnd ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][( ·𝑠𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))}
821, 81wceq 1528 1 wff SLMod = {𝑔 ∈ CMnd ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][( ·𝑠𝑔) / 𝑠][(Scalar‘𝑔) / 𝑓][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ SRing ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤 ∧ ((0g𝑓)𝑠𝑤) = (0g𝑔))))}
Colors of variables: wff setvar class
This definition is referenced by:  isslmd  30758
  Copyright terms: Public domain W3C validator