# 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}\mathrm{AssAlg}$
1 vw ${setvar}{w}$
2 clmod ${class}\mathrm{LMod}$
3 crg ${class}\mathrm{Ring}$
4 2 3 cin ${class}\left(\mathrm{LMod}\cap \mathrm{Ring}\right)$
5 csca ${class}\mathrm{Scalar}$
6 1 cv ${setvar}{w}$
7 6 5 cfv ${class}\mathrm{Scalar}\left({w}\right)$
8 vf ${setvar}{f}$
9 8 cv ${setvar}{f}$
10 ccrg ${class}\mathrm{CRing}$
11 9 10 wcel ${wff}{f}\in \mathrm{CRing}$
12 vr ${setvar}{r}$
13 cbs ${class}\mathrm{Base}$
14 9 13 cfv ${class}{\mathrm{Base}}_{{f}}$
15 vx ${setvar}{x}$
16 6 13 cfv ${class}{\mathrm{Base}}_{{w}}$
17 vy ${setvar}{y}$
18 cvsca ${class}{\cdot }_{𝑠}$
19 6 18 cfv ${class}{\cdot }_{{w}}$
20 vs ${setvar}{s}$
21 cmulr ${class}{\cdot }_{𝑟}$
22 6 21 cfv ${class}{\cdot }_{{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}\left({r}{s}{x}\right)$
28 23 cv ${setvar}{t}$
29 17 cv ${setvar}{y}$
30 27 29 28 co ${class}\left(\left({r}{s}{x}\right){t}{y}\right)$
31 26 29 28 co ${class}\left({x}{t}{y}\right)$
32 24 31 25 co ${class}\left({r}{s}\left({x}{t}{y}\right)\right)$
33 30 32 wceq ${wff}\left({r}{s}{x}\right){t}{y}={r}{s}\left({x}{t}{y}\right)$
34 24 29 25 co ${class}\left({r}{s}{y}\right)$
35 26 34 28 co ${class}\left({x}{t}\left({r}{s}{y}\right)\right)$
36 35 32 wceq ${wff}{x}{t}\left({r}{s}{y}\right)={r}{s}\left({x}{t}{y}\right)$
37 33 36 wa ${wff}\left(\left({r}{s}{x}\right){t}{y}={r}{s}\left({x}{t}{y}\right)\wedge {x}{t}\left({r}{s}{y}\right)={r}{s}\left({x}{t}{y}\right)\right)$
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