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 32341
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 32340 . 2 class SLMod
2 vf . . . . . . . . . . . . 13 setvar 𝑓
32cv 1540 . . . . . . . . . . . 12 class 𝑓
4 csrg 20008 . . . . . . . . . . . 12 class SRing
53, 4wcel 2106 . . . . . . . . . . 11 wff 𝑓 ∈ SRing
6 vr . . . . . . . . . . . . . . . . . . . 20 setvar π‘Ÿ
76cv 1540 . . . . . . . . . . . . . . . . . . 19 class π‘Ÿ
8 vw . . . . . . . . . . . . . . . . . . . 20 setvar 𝑀
98cv 1540 . . . . . . . . . . . . . . . . . . 19 class 𝑀
10 vs . . . . . . . . . . . . . . . . . . . 20 setvar 𝑠
1110cv 1540 . . . . . . . . . . . . . . . . . . 19 class 𝑠
127, 9, 11co 7408 . . . . . . . . . . . . . . . . . 18 class (π‘Ÿπ‘ π‘€)
13 vv . . . . . . . . . . . . . . . . . . 19 setvar 𝑣
1413cv 1540 . . . . . . . . . . . . . . . . . 18 class 𝑣
1512, 14wcel 2106 . . . . . . . . . . . . . . . . 17 wff (π‘Ÿπ‘ π‘€) ∈ 𝑣
16 vx . . . . . . . . . . . . . . . . . . . . 21 setvar π‘₯
1716cv 1540 . . . . . . . . . . . . . . . . . . . 20 class π‘₯
18 va . . . . . . . . . . . . . . . . . . . . 21 setvar π‘Ž
1918cv 1540 . . . . . . . . . . . . . . . . . . . 20 class π‘Ž
209, 17, 19co 7408 . . . . . . . . . . . . . . . . . . 19 class (π‘€π‘Žπ‘₯)
217, 20, 11co 7408 . . . . . . . . . . . . . . . . . 18 class (π‘Ÿπ‘ (π‘€π‘Žπ‘₯))
227, 17, 11co 7408 . . . . . . . . . . . . . . . . . . 19 class (π‘Ÿπ‘ π‘₯)
2312, 22, 19co 7408 . . . . . . . . . . . . . . . . . 18 class ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯))
2421, 23wceq 1541 . . . . . . . . . . . . . . . . 17 wff (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯))
25 vq . . . . . . . . . . . . . . . . . . . . 21 setvar π‘ž
2625cv 1540 . . . . . . . . . . . . . . . . . . . 20 class π‘ž
27 vp . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑝
2827cv 1540 . . . . . . . . . . . . . . . . . . . 20 class 𝑝
2926, 7, 28co 7408 . . . . . . . . . . . . . . . . . . 19 class (π‘žπ‘π‘Ÿ)
3029, 9, 11co 7408 . . . . . . . . . . . . . . . . . 18 class ((π‘žπ‘π‘Ÿ)𝑠𝑀)
3126, 9, 11co 7408 . . . . . . . . . . . . . . . . . . 19 class (π‘žπ‘ π‘€)
3231, 12, 19co 7408 . . . . . . . . . . . . . . . . . 18 class ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))
3330, 32wceq 1541 . . . . . . . . . . . . . . . . 17 wff ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))
3415, 24, 33w3a 1087 . . . . . . . . . . . . . . . 16 wff ((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€)))
35 vt . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑑
3635cv 1540 . . . . . . . . . . . . . . . . . . . 20 class 𝑑
3726, 7, 36co 7408 . . . . . . . . . . . . . . . . . . 19 class (π‘žπ‘‘π‘Ÿ)
3837, 9, 11co 7408 . . . . . . . . . . . . . . . . . 18 class ((π‘žπ‘‘π‘Ÿ)𝑠𝑀)
3926, 12, 11co 7408 . . . . . . . . . . . . . . . . . 18 class (π‘žπ‘ (π‘Ÿπ‘ π‘€))
4038, 39wceq 1541 . . . . . . . . . . . . . . . . 17 wff ((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€))
41 cur 20003 . . . . . . . . . . . . . . . . . . . 20 class 1r
423, 41cfv 6543 . . . . . . . . . . . . . . . . . . 19 class (1rβ€˜π‘“)
4342, 9, 11co 7408 . . . . . . . . . . . . . . . . . 18 class ((1rβ€˜π‘“)𝑠𝑀)
4443, 9wceq 1541 . . . . . . . . . . . . . . . . 17 wff ((1rβ€˜π‘“)𝑠𝑀) = 𝑀
45 c0g 17384 . . . . . . . . . . . . . . . . . . . 20 class 0g
463, 45cfv 6543 . . . . . . . . . . . . . . . . . . 19 class (0gβ€˜π‘“)
4746, 9, 11co 7408 . . . . . . . . . . . . . . . . . 18 class ((0gβ€˜π‘“)𝑠𝑀)
48 vg . . . . . . . . . . . . . . . . . . . 20 setvar 𝑔
4948cv 1540 . . . . . . . . . . . . . . . . . . 19 class 𝑔
5049, 45cfv 6543 . . . . . . . . . . . . . . . . . 18 class (0gβ€˜π‘”)
5147, 50wceq 1541 . . . . . . . . . . . . . . . . 17 wff ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)
5240, 44, 51w3a 1087 . . . . . . . . . . . . . . . 16 wff (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))
5334, 52wa 396 . . . . . . . . . . . . . . 15 wff (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))
5453, 8, 14wral 3061 . . . . . . . . . . . . . 14 wff βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))
5554, 16, 14wral 3061 . . . . . . . . . . . . 13 wff βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))
56 vk . . . . . . . . . . . . . 14 setvar π‘˜
5756cv 1540 . . . . . . . . . . . . 13 class π‘˜
5855, 6, 57wral 3061 . . . . . . . . . . . 12 wff βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))
5958, 25, 57wral 3061 . . . . . . . . . . 11 wff βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”)))
605, 59wa 396 . . . . . . . . . 10 wff (𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))
61 cmulr 17197 . . . . . . . . . . 11 class .r
623, 61cfv 6543 . . . . . . . . . 10 class (.rβ€˜π‘“)
6360, 35, 62wsbc 3777 . . . . . . . . 9 wff [(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))
64 cplusg 17196 . . . . . . . . . 10 class +g
653, 64cfv 6543 . . . . . . . . 9 class (+gβ€˜π‘“)
6663, 27, 65wsbc 3777 . . . . . . . 8 wff [(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))
67 cbs 17143 . . . . . . . . 9 class Base
683, 67cfv 6543 . . . . . . . 8 class (Baseβ€˜π‘“)
6966, 56, 68wsbc 3777 . . . . . . 7 wff [(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))
70 csca 17199 . . . . . . . 8 class Scalar
7149, 70cfv 6543 . . . . . . 7 class (Scalarβ€˜π‘”)
7269, 2, 71wsbc 3777 . . . . . 6 wff [(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))
73 cvsca 17200 . . . . . . 7 class ·𝑠
7449, 73cfv 6543 . . . . . 6 class ( ·𝑠 β€˜π‘”)
7572, 10, 74wsbc 3777 . . . . 5 wff [( ·𝑠 β€˜π‘”) / 𝑠][(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))
7649, 64cfv 6543 . . . . 5 class (+gβ€˜π‘”)
7775, 18, 76wsbc 3777 . . . 4 wff [(+gβ€˜π‘”) / π‘Ž][( ·𝑠 β€˜π‘”) / 𝑠][(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))
7849, 67cfv 6543 . . . 4 class (Baseβ€˜π‘”)
7977, 13, 78wsbc 3777 . . 3 wff [(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / π‘Ž][( ·𝑠 β€˜π‘”) / 𝑠][(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))
80 ccmn 19647 . . 3 class CMnd
8179, 48, 80crab 3432 . 2 class {𝑔 ∈ CMnd ∣ [(Baseβ€˜π‘”) / 𝑣][(+gβ€˜π‘”) / π‘Ž][( ·𝑠 β€˜π‘”) / 𝑠][(Scalarβ€˜π‘”) / 𝑓][(Baseβ€˜π‘“) / π‘˜][(+gβ€˜π‘“) / 𝑝][(.rβ€˜π‘“) / 𝑑](𝑓 ∈ SRing ∧ βˆ€π‘ž ∈ π‘˜ βˆ€π‘Ÿ ∈ π‘˜ βˆ€π‘₯ ∈ 𝑣 βˆ€π‘€ ∈ 𝑣 (((π‘Ÿπ‘ π‘€) ∈ 𝑣 ∧ (π‘Ÿπ‘ (π‘€π‘Žπ‘₯)) = ((π‘Ÿπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘₯)) ∧ ((π‘žπ‘π‘Ÿ)𝑠𝑀) = ((π‘žπ‘ π‘€)π‘Ž(π‘Ÿπ‘ π‘€))) ∧ (((π‘žπ‘‘π‘Ÿ)𝑠𝑀) = (π‘žπ‘ (π‘Ÿπ‘ π‘€)) ∧ ((1rβ€˜π‘“)𝑠𝑀) = 𝑀 ∧ ((0gβ€˜π‘“)𝑠𝑀) = (0gβ€˜π‘”))))}
821, 81wceq 1541 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  32342
  Copyright terms: Public domain W3C validator