# Metamath Proof Explorer

## Theorem zlmvsca

Description: Scalar multiplication operation of a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses zlmbas.w
`|- W = ( ZMod ` G )`
zlmvsca.2
`|- .x. = ( .g ` G )`
Assertion zlmvsca
`|- .x. = ( .s ` W )`

### Proof

Step Hyp Ref Expression
1 zlmbas.w
` |-  W = ( ZMod ` G )`
2 zlmvsca.2
` |-  .x. = ( .g ` G )`
3 ovex
` |-  ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) e. _V`
4 2 fvexi
` |-  .x. e. _V`
5 vscaid
` |-  .s = Slot ( .s ` ndx )`
6 5 setsid
` |-  ( ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) e. _V /\ .x. e. _V ) -> .x. = ( .s ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) ) )`
7 3 4 6 mp2an
` |-  .x. = ( .s ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )`
8 1 2 zlmval
` |-  ( G e. _V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )`
9 8 fveq2d
` |-  ( G e. _V -> ( .s ` W ) = ( .s ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) ) )`
10 7 9 eqtr4id
` |-  ( G e. _V -> .x. = ( .s ` W ) )`
11 5 str0
` |-  (/) = ( .s ` (/) )`
12 fvprc
` |-  ( -. G e. _V -> ( .g ` G ) = (/) )`
13 2 12 syl5eq
` |-  ( -. G e. _V -> .x. = (/) )`
14 fvprc
` |-  ( -. G e. _V -> ( ZMod ` G ) = (/) )`
15 1 14 syl5eq
` |-  ( -. G e. _V -> W = (/) )`
16 15 fveq2d
` |-  ( -. G e. _V -> ( .s ` W ) = ( .s ` (/) ) )`
17 11 13 16 3eqtr4a
` |-  ( -. G e. _V -> .x. = ( .s ` W ) )`
18 10 17 pm2.61i
` |-  .x. = ( .s ` W )`