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 
|- AssAlg = { w e. ( LMod i^i Ring ) | [. ( Scalar ` w ) / f ]. ( f e. CRing /\ A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 casa 
 |-  AssAlg
1 vw 
 |-  w
2 clmod 
 |-  LMod
3 crg 
 |-  Ring
4 2 3 cin 
 |-  ( LMod i^i Ring )
5 csca 
 |-  Scalar
6 1 cv 
 |-  w
7 6 5 cfv 
 |-  ( Scalar ` w )
8 vf 
 |-  f
9 8 cv 
 |-  f
10 ccrg 
 |-  CRing
11 9 10 wcel 
 |-  f e. CRing
12 vr 
 |-  r
13 cbs 
 |-  Base
14 9 13 cfv 
 |-  ( Base ` f )
15 vx 
 |-  x
16 6 13 cfv 
 |-  ( Base ` w )
17 vy 
 |-  y
18 cvsca 
 |-  .s
19 6 18 cfv 
 |-  ( .s ` w )
20 vs 
 |-  s
21 cmulr 
 |-  .r
22 6 21 cfv 
 |-  ( .r ` w )
23 vt 
 |-  t
24 12 cv 
 |-  r
25 20 cv 
 |-  s
26 15 cv 
 |-  x
27 24 26 25 co 
 |-  ( r s x )
28 23 cv 
 |-  t
29 17 cv 
 |-  y
30 27 29 28 co 
 |-  ( ( r s x ) t y )
31 26 29 28 co 
 |-  ( x t y )
32 24 31 25 co 
 |-  ( r s ( x t y ) )
33 30 32 wceq 
 |-  ( ( r s x ) t y ) = ( r s ( x t y ) )
34 24 29 25 co 
 |-  ( r s y )
35 26 34 28 co 
 |-  ( x t ( r s y ) )
36 35 32 wceq 
 |-  ( x t ( r s y ) ) = ( r s ( x t y ) )
37 33 36 wa 
 |-  ( ( ( 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 
 |-  [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
39 38 20 19 wsbc 
 |-  [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
40 39 17 16 wral 
 |-  A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
41 40 15 16 wral 
 |-  A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
42 41 12 14 wral 
 |-  A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) )
43 11 42 wa 
 |-  ( f e. CRing /\ A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) )
44 43 8 7 wsbc 
 |-  [. ( Scalar ` w ) / f ]. ( f e. CRing /\ A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) )
45 44 1 4 crab 
 |-  { w e. ( LMod i^i Ring ) | [. ( Scalar ` w ) / f ]. ( f e. CRing /\ A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) ) }
46 0 45 wceq 
 |-  AssAlg = { w e. ( LMod i^i Ring ) | [. ( Scalar ` w ) / f ]. ( f e. CRing /\ A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) ) }