Metamath Proof Explorer

Theorem zlmsca

Description: Scalar ring of a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 12-Jun-2019) (Proof shortened by AV, 2-Nov-2024)

Ref Expression
Hypothesis zlmbas.w 
|- W = ( ZMod ` G )
Assertion zlmsca 
|- ( G e. V -> ZZring = ( Scalar ` W ) )

Proof

Step Hyp Ref Expression
1 zlmbas.w 
 |-  W = ( ZMod ` G )
2 scaid 
 |-  Scalar = Slot ( Scalar ` ndx )
3 vscandxnscandx 
 |-  ( .s ` ndx ) =/= ( Scalar ` ndx )
4 3 necomi 
 |-  ( Scalar ` ndx ) =/= ( .s ` ndx )
5 2 4 setsnid 
 |-  ( Scalar ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) = ( Scalar ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
6 zringring 
 |-  ZZring e. Ring
7 2 setsid 
 |-  ( ( G e. V /\ ZZring e. Ring ) -> ZZring = ( Scalar ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) )
8 6 7 mpan2 
 |-  ( G e. V -> ZZring = ( Scalar ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) )
9 eqid 
 |-  ( .g ` G ) = ( .g ` G )
10 1 9 zlmval 
 |-  ( G e. V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
11 10 fveq2d 
 |-  ( G e. V -> ( Scalar ` W ) = ( Scalar ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) ) )
12 5 8 11 3eqtr4a 
 |-  ( G e. V -> ZZring = ( Scalar ` W ) )