# 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}=\mathrm{ℤMod}\left({G}\right)$
Assertion zlmsca ${⊢}{G}\in {V}\to {ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left({W}\right)$

### Proof

Step Hyp Ref Expression
1 zlmbas.w ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
2 scaid ${⊢}\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$
3 5re ${⊢}5\in ℝ$
4 5lt6 ${⊢}5<6$
5 3 4 ltneii ${⊢}5\ne 6$
6 scandx ${⊢}\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$
7 vscandx ${⊢}{\cdot }_{\mathrm{ndx}}=6$
8 6 7 neeq12i ${⊢}\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}↔5\ne 6$
9 5 8 mpbir ${⊢}\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$
10 2 9 setsnid ${⊢}\mathrm{Scalar}\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)=\mathrm{Scalar}\left(\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{G}}⟩\right)$
11 zringring ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{Ring}$
12 2 setsid ${⊢}\left({G}\in {V}\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{Ring}\right)\to {ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)$
13 11 12 mpan2 ${⊢}{G}\in {V}\to {ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)$
14 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
15 1 14 zlmval ${⊢}{G}\in {V}\to {W}=\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{G}}⟩$
16 15 fveq2d ${⊢}{G}\in {V}\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left(\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{G}}⟩\right)$
17 10 13 16 3eqtr4a ${⊢}{G}\in {V}\to {ℤ}_{\mathrm{ring}}=\mathrm{Scalar}\left({W}\right)$