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 eqtrid 
 |-  ( -. G e. _V -> .x. = (/) )
14 fvprc 
 |-  ( -. G e. _V -> ( ZMod ` G ) = (/) )
15 1 14 eqtrid 
 |-  ( -. 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 )