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

Definition df-assa 17308
 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 Scalar
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-assa
StepHypRef Expression
1 casa 17305 . 2 AssAlg
2 vf . . . . . . 7
32cv 1363 . . . . . 6
4 ccrg 16580 . . . . . 6
53, 4wcel 1757 . . . . 5
6 vr . . . . . . . . . . . . . . 15
76cv 1363 . . . . . . . . . . . . . 14
8 vx . . . . . . . . . . . . . . 15
98cv 1363 . . . . . . . . . . . . . 14
10 vs . . . . . . . . . . . . . . 15
1110cv 1363 . . . . . . . . . . . . . 14
127, 9, 11co 6082 . . . . . . . . . . . . 13
13 vy . . . . . . . . . . . . . 14
1413cv 1363 . . . . . . . . . . . . 13
15 vt . . . . . . . . . . . . . 14
1615cv 1363 . . . . . . . . . . . . 13
1712, 14, 16co 6082 . . . . . . . . . . . 12
189, 14, 16co 6082 . . . . . . . . . . . . 13
197, 18, 11co 6082 . . . . . . . . . . . 12
2017, 19wceq 1364 . . . . . . . . . . 11
217, 14, 11co 6082 . . . . . . . . . . . . 13
229, 21, 16co 6082 . . . . . . . . . . . 12
2322, 19wceq 1364 . . . . . . . . . . 11
2420, 23wa 369 . . . . . . . . . 10
25 vw . . . . . . . . . . . 12
2625cv 1363 . . . . . . . . . . 11
27 cmulr 14224 . . . . . . . . . . 11
2826, 27cfv 5408 . . . . . . . . . 10
2924, 15, 28wsbc 3177 . . . . . . . . 9
30 cvsca 14227 . . . . . . . . . 10
3126, 30cfv 5408 . . . . . . . . 9
3229, 10, 31wsbc 3177 . . . . . . . 8
33 cbs 14159 . . . . . . . . 9
3426, 33cfv 5408 . . . . . . . 8
3532, 13, 34wral 2707 . . . . . . 7
3635, 8, 34wral 2707 . . . . . 6
373, 33cfv 5408 . . . . . 6
3836, 6, 37wral 2707 . . . . 5
395, 38wa 369 . . . 4
40 csca 14226 . . . . 5 Scalar
4126, 40cfv 5408 . . . 4 Scalar
4239, 2, 41wsbc 3177 . . 3 Scalar
43 clmod 16874 . . . 4
44 crg 16579 . . . 4
4543, 44cin 3317 . . 3
4642, 25, 45crab 2711 . 2 Scalar
471, 46wceq 1364 1 AssAlg Scalar
 Colors of variables: wff setvar class This definition is referenced by:  isassa  17311
 Copyright terms: Public domain W3C validator