Description: The ZZ-module ZZ X. ZZ is a (left) module with the ring of integers as base set. (Contributed by AV, 20-May-2019) (Revised by AV, 10-Jun-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | zlmodzxz.z | |- Z = ( ZZring freeLMod { 0 , 1 } ) |
|
| Assertion | zlmodzxzlmod | |- ( Z e. LMod /\ ZZring = ( Scalar ` Z ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zlmodzxz.z | |- Z = ( ZZring freeLMod { 0 , 1 } ) |
|
| 2 | zringring | |- ZZring e. Ring |
|
| 3 | prex | |- { 0 , 1 } e. _V |
|
| 4 | 1 | frlmlmod | |- ( ( ZZring e. Ring /\ { 0 , 1 } e. _V ) -> Z e. LMod ) |
| 5 | 2 3 4 | mp2an | |- Z e. LMod |
| 6 | 1 | frlmsca | |- ( ( ZZring e. Ring /\ { 0 , 1 } e. _V ) -> ZZring = ( Scalar ` Z ) ) |
| 7 | 2 3 6 | mp2an | |- ZZring = ( Scalar ` Z ) |
| 8 | 5 7 | pm3.2i | |- ( Z e. LMod /\ ZZring = ( Scalar ` Z ) ) |