MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-assa Structured version   Visualization version   GIF version

Definition df-assa 21407
Description: Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.)
Assertion
Ref Expression
df-assa AssAlg = {𝑀 ∈ (LMod ∩ Ring) ∣ [(Scalarβ€˜π‘€) / 𝑓]βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))}
Distinct variable group:   𝑓,π‘Ÿ,𝑠,𝑑,𝑀,π‘₯,𝑦

Detailed syntax breakdown of Definition df-assa
StepHypRef Expression
1 casa 21404 . 2 class AssAlg
2 vr . . . . . . . . . . . . . 14 setvar π‘Ÿ
32cv 1540 . . . . . . . . . . . . 13 class π‘Ÿ
4 vx . . . . . . . . . . . . . 14 setvar π‘₯
54cv 1540 . . . . . . . . . . . . 13 class π‘₯
6 vs . . . . . . . . . . . . . 14 setvar 𝑠
76cv 1540 . . . . . . . . . . . . 13 class 𝑠
83, 5, 7co 7408 . . . . . . . . . . . 12 class (π‘Ÿπ‘ π‘₯)
9 vy . . . . . . . . . . . . 13 setvar 𝑦
109cv 1540 . . . . . . . . . . . 12 class 𝑦
11 vt . . . . . . . . . . . . 13 setvar 𝑑
1211cv 1540 . . . . . . . . . . . 12 class 𝑑
138, 10, 12co 7408 . . . . . . . . . . 11 class ((π‘Ÿπ‘ π‘₯)𝑑𝑦)
145, 10, 12co 7408 . . . . . . . . . . . 12 class (π‘₯𝑑𝑦)
153, 14, 7co 7408 . . . . . . . . . . 11 class (π‘Ÿπ‘ (π‘₯𝑑𝑦))
1613, 15wceq 1541 . . . . . . . . . 10 wff ((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))
173, 10, 7co 7408 . . . . . . . . . . . 12 class (π‘Ÿπ‘ π‘¦)
185, 17, 12co 7408 . . . . . . . . . . 11 class (π‘₯𝑑(π‘Ÿπ‘ π‘¦))
1918, 15wceq 1541 . . . . . . . . . 10 wff (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦))
2016, 19wa 396 . . . . . . . . 9 wff (((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))
21 vw . . . . . . . . . . 11 setvar 𝑀
2221cv 1540 . . . . . . . . . 10 class 𝑀
23 cmulr 17197 . . . . . . . . . 10 class .r
2422, 23cfv 6543 . . . . . . . . 9 class (.rβ€˜π‘€)
2520, 11, 24wsbc 3777 . . . . . . . 8 wff [(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))
26 cvsca 17200 . . . . . . . . 9 class ·𝑠
2722, 26cfv 6543 . . . . . . . 8 class ( ·𝑠 β€˜π‘€)
2825, 6, 27wsbc 3777 . . . . . . 7 wff [( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))
29 cbs 17143 . . . . . . . 8 class Base
3022, 29cfv 6543 . . . . . . 7 class (Baseβ€˜π‘€)
3128, 9, 30wral 3061 . . . . . 6 wff βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))
3231, 4, 30wral 3061 . . . . 5 wff βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))
33 vf . . . . . . 7 setvar 𝑓
3433cv 1540 . . . . . 6 class 𝑓
3534, 29cfv 6543 . . . . 5 class (Baseβ€˜π‘“)
3632, 2, 35wral 3061 . . . 4 wff βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))
37 csca 17199 . . . . 5 class Scalar
3822, 37cfv 6543 . . . 4 class (Scalarβ€˜π‘€)
3936, 33, 38wsbc 3777 . . 3 wff [(Scalarβ€˜π‘€) / 𝑓]βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))
40 clmod 20470 . . . 4 class LMod
41 crg 20055 . . . 4 class Ring
4240, 41cin 3947 . . 3 class (LMod ∩ Ring)
4339, 21, 42crab 3432 . 2 class {𝑀 ∈ (LMod ∩ Ring) ∣ [(Scalarβ€˜π‘€) / 𝑓]βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))}
441, 43wceq 1541 1 wff AssAlg = {𝑀 ∈ (LMod ∩ Ring) ∣ [(Scalarβ€˜π‘€) / 𝑓]βˆ€π‘Ÿ ∈ (Baseβ€˜π‘“)βˆ€π‘₯ ∈ (Baseβ€˜π‘€)βˆ€π‘¦ ∈ (Baseβ€˜π‘€)[( ·𝑠 β€˜π‘€) / 𝑠][(.rβ€˜π‘€) / 𝑑](((π‘Ÿπ‘ π‘₯)𝑑𝑦) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)) ∧ (π‘₯𝑑(π‘Ÿπ‘ π‘¦)) = (π‘Ÿπ‘ (π‘₯𝑑𝑦)))}
Colors of variables: wff setvar class
This definition is referenced by:  isassa  21410
  Copyright terms: Public domain W3C validator