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. >. ) )