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 20671
Description: Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a (commutative) 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.)
Assertion
Ref Expression
df-assa AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}
Distinct variable group:   𝑓,𝑟,𝑠,𝑡,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-assa
StepHypRef Expression
1 casa 20668 . 2 class AssAlg
2 vf . . . . . . 7 setvar 𝑓
32cv 1541 . . . . . 6 class 𝑓
4 ccrg 19419 . . . . . 6 class CRing
53, 4wcel 2114 . . . . 5 wff 𝑓 ∈ CRing
6 vr . . . . . . . . . . . . . . 15 setvar 𝑟
76cv 1541 . . . . . . . . . . . . . 14 class 𝑟
8 vx . . . . . . . . . . . . . . 15 setvar 𝑥
98cv 1541 . . . . . . . . . . . . . 14 class 𝑥
10 vs . . . . . . . . . . . . . . 15 setvar 𝑠
1110cv 1541 . . . . . . . . . . . . . 14 class 𝑠
127, 9, 11co 7172 . . . . . . . . . . . . 13 class (𝑟𝑠𝑥)
13 vy . . . . . . . . . . . . . 14 setvar 𝑦
1413cv 1541 . . . . . . . . . . . . 13 class 𝑦
15 vt . . . . . . . . . . . . . 14 setvar 𝑡
1615cv 1541 . . . . . . . . . . . . 13 class 𝑡
1712, 14, 16co 7172 . . . . . . . . . . . 12 class ((𝑟𝑠𝑥)𝑡𝑦)
189, 14, 16co 7172 . . . . . . . . . . . . 13 class (𝑥𝑡𝑦)
197, 18, 11co 7172 . . . . . . . . . . . 12 class (𝑟𝑠(𝑥𝑡𝑦))
2017, 19wceq 1542 . . . . . . . . . . 11 wff ((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦))
217, 14, 11co 7172 . . . . . . . . . . . . 13 class (𝑟𝑠𝑦)
229, 21, 16co 7172 . . . . . . . . . . . 12 class (𝑥𝑡(𝑟𝑠𝑦))
2322, 19wceq 1542 . . . . . . . . . . 11 wff (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))
2420, 23wa 399 . . . . . . . . . 10 wff (((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
25 vw . . . . . . . . . . . 12 setvar 𝑤
2625cv 1541 . . . . . . . . . . 11 class 𝑤
27 cmulr 16671 . . . . . . . . . . 11 class .r
2826, 27cfv 6339 . . . . . . . . . 10 class (.r𝑤)
2924, 15, 28wsbc 3680 . . . . . . . . 9 wff [(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
30 cvsca 16674 . . . . . . . . . 10 class ·𝑠
3126, 30cfv 6339 . . . . . . . . 9 class ( ·𝑠𝑤)
3229, 10, 31wsbc 3680 . . . . . . . 8 wff [( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
33 cbs 16588 . . . . . . . . 9 class Base
3426, 33cfv 6339 . . . . . . . 8 class (Base‘𝑤)
3532, 13, 34wral 3053 . . . . . . 7 wff 𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
3635, 8, 34wral 3053 . . . . . 6 wff 𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
373, 33cfv 6339 . . . . . 6 class (Base‘𝑓)
3836, 6, 37wral 3053 . . . . 5 wff 𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦)))
395, 38wa 399 . . . 4 wff (𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))
40 csca 16673 . . . . 5 class Scalar
4126, 40cfv 6339 . . . 4 class (Scalar‘𝑤)
4239, 2, 41wsbc 3680 . . 3 wff [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))
43 clmod 19755 . . . 4 class LMod
44 crg 19418 . . . 4 class Ring
4543, 44cin 3842 . . 3 class (LMod ∩ Ring)
4642, 25, 45crab 3057 . 2 class {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}
471, 46wceq 1542 1 wff AssAlg = {𝑤 ∈ (LMod ∩ Ring) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ CRing ∧ ∀𝑟 ∈ (Base‘𝑓)∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑤)[( ·𝑠𝑤) / 𝑠][(.r𝑤) / 𝑡](((𝑟𝑠𝑥)𝑡𝑦) = (𝑟𝑠(𝑥𝑡𝑦)) ∧ (𝑥𝑡(𝑟𝑠𝑦)) = (𝑟𝑠(𝑥𝑡𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  isassa  20674
  Copyright terms: Public domain W3C validator