Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
2 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
3 |
|
eqid |
|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
4 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
5 |
|
eqid |
|- ( .r ` W ) = ( .r ` W ) |
6 |
1 2 3 4 5
|
isassa |
|- ( W e. AssAlg <-> ( ( W e. LMod /\ W e. Ring /\ ( Scalar ` W ) e. CRing ) /\ A. z e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( ( z ( .s ` W ) x ) ( .r ` W ) y ) = ( z ( .s ` W ) ( x ( .r ` W ) y ) ) /\ ( x ( .r ` W ) ( z ( .s ` W ) y ) ) = ( z ( .s ` W ) ( x ( .r ` W ) y ) ) ) ) ) |
7 |
6
|
simplbi |
|- ( W e. AssAlg -> ( W e. LMod /\ W e. Ring /\ ( Scalar ` W ) e. CRing ) ) |
8 |
7
|
simp2d |
|- ( W e. AssAlg -> W e. Ring ) |