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)

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 5re 
 |-  5 e. RR
4 5lt6 
 |-  5 < 6
5 3 4 ltneii 
 |-  5 =/= 6
6 scandx 
 |-  ( Scalar ` ndx ) = 5
7 vscandx 
 |-  ( .s ` ndx ) = 6
8 6 7 neeq12i 
 |-  ( ( Scalar ` ndx ) =/= ( .s ` ndx ) <-> 5 =/= 6 )
9 5 8 mpbir 
 |-  ( Scalar ` ndx ) =/= ( .s ` ndx )
10 2 9 setsnid 
 |-  ( Scalar ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) = ( Scalar ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
11 zringring 
 |-  ZZring e. Ring
12 2 setsid 
 |-  ( ( G e. V /\ ZZring e. Ring ) -> ZZring = ( Scalar ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) )
13 11 12 mpan2 
 |-  ( G e. V -> ZZring = ( Scalar ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) )
14 eqid 
 |-  ( .g ` G ) = ( .g ` G )
15 1 14 zlmval 
 |-  ( G e. V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
16 15 fveq2d 
 |-  ( G e. V -> ( Scalar ` W ) = ( Scalar ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) ) )
17 10 13 16 3eqtr4a 
 |-  ( G e. V -> ZZring = ( Scalar ` W ) )