This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zlmval

Description: Augment an abelian group with vector space operations to turn it into a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 12-Jun-2019)

Ref Expression
Hypotheses zlmval.w 
|- W = ( ZMod ` G )
zlmval.m 
|- .x. = ( .g ` G )
Assertion zlmval 
|- ( G e. V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )

Proof

Step Hyp Ref Expression
1 zlmval.w 
 |-  W = ( ZMod ` G )
2 zlmval.m 
 |-  .x. = ( .g ` G )
3 elex 
 |-  ( G e. V -> G e. _V )
4 oveq1 
 |-  ( g = G -> ( g sSet <. ( Scalar ` ndx ) , ZZring >. ) = ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) )
5 fveq2 
 |-  ( g = G -> ( .g ` g ) = ( .g ` G ) )
6 5 2 eqtr4di 
 |-  ( g = G -> ( .g ` g ) = .x. )
7 6 opeq2d 
 |-  ( g = G -> <. ( .s ` ndx ) , ( .g ` g ) >. = <. ( .s ` ndx ) , .x. >. )
8 4 7 oveq12d 
 |-  ( g = G -> ( ( g sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` g ) >. ) = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )
9 df-zlm 
 |-  ZMod = ( g e. _V |-> ( ( g sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` g ) >. ) )
10 ovex 
 |-  ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) e. _V
11 8 9 10 fvmpt 
 |-  ( G e. _V -> ( ZMod ` G ) = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )
12 3 11 syl 
 |-  ( G e. V -> ( ZMod ` G ) = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )
13 1 12 eqtrid 
 |-  ( G e. V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )