Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
2 |
|
eqid |
|- ( +g ` W ) = ( +g ` W ) |
3 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
4 |
|
eqid |
|- ( 0g ` W ) = ( 0g ` W ) |
5 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
6 |
|
eqid |
|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
7 |
|
eqid |
|- ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) ) |
8 |
|
eqid |
|- ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) ) |
9 |
|
eqid |
|- ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) ) |
10 |
|
eqid |
|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) ) |
11 |
1 2 3 4 5 6 7 8 9 10
|
isslmd |
|- ( W e. SLMod <-> ( W e. CMnd /\ ( Scalar ` W ) e. SRing /\ A. w e. ( Base ` ( Scalar ` W ) ) A. z e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( ( z ( .s ` W ) y ) e. ( Base ` W ) /\ ( z ( .s ` W ) ( y ( +g ` W ) x ) ) = ( ( z ( .s ` W ) y ) ( +g ` W ) ( z ( .s ` W ) x ) ) /\ ( ( w ( +g ` ( Scalar ` W ) ) z ) ( .s ` W ) y ) = ( ( w ( .s ` W ) y ) ( +g ` W ) ( z ( .s ` W ) y ) ) ) /\ ( ( ( w ( .r ` ( Scalar ` W ) ) z ) ( .s ` W ) y ) = ( w ( .s ` W ) ( z ( .s ` W ) y ) ) /\ ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) y ) = y /\ ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) y ) = ( 0g ` W ) ) ) ) ) |
12 |
11
|
simp1bi |
|- ( W e. SLMod -> W e. CMnd ) |