# 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 ) )`