# Metamath Proof Explorer

## Definition df-assa

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)

Ref Expression
Assertion df-assa

### Detailed syntax breakdown

Step Hyp Ref Expression
0 casa $class AssAlg$
1 vw $setvar w$
2 clmod $class LMod$
3 crg $class Ring$
4 2 3 cin $class LMod ∩ Ring$
5 csca $class Scalar$
6 1 cv $setvar w$
7 6 5 cfv $class Scalar ⁡ w$
8 vf $setvar f$
9 8 cv $setvar f$
10 ccrg $class CRing$
11 9 10 wcel $wff f ∈ CRing$
12 vr $setvar r$
13 cbs $class Base$
14 9 13 cfv $class Base f$
15 vx $setvar x$
16 6 13 cfv $class Base w$
17 vy $setvar y$
18 cvsca $class ⋅ 𝑠$
19 6 18 cfv $class ⋅ w$
20 vs $setvar s$
21 cmulr $class ⋅ 𝑟$
22 6 21 cfv $class ⋅ w$
23 vt $setvar t$
24 12 cv $setvar r$
25 20 cv $setvar s$
26 15 cv $setvar x$
27 24 26 25 co $class r s x$
28 23 cv $setvar t$
29 17 cv $setvar y$
30 27 29 28 co $class r s x t y$
31 26 29 28 co $class x t y$
32 24 31 25 co $class r s x t y$
33 30 32 wceq $wff r s x t y = r s x t y$
34 24 29 25 co $class r s y$
35 26 34 28 co $class x t r s y$
36 35 32 wceq $wff x t r s y = r s x t y$
37 33 36 wa $wff r s x t y = r s x t y ∧ x t r s y = r s x t y$
38 37 23 22 wsbc
39 38 20 19 wsbc
40 39 17 16 wral
41 40 15 16 wral
42 41 12 14 wral
43 11 42 wa
44 43 8 7 wsbc
45 44 1 4 crab
46 0 45 wceq