# 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 𝑊 = ( ℤMod ‘ 𝐺 )
Assertion zlmsca ( 𝐺𝑉 → ℤring = ( Scalar ‘ 𝑊 ) )

### Proof

Step Hyp Ref Expression
1 zlmbas.w 𝑊 = ( ℤMod ‘ 𝐺 )
2 scaid Scalar = Slot ( Scalar ‘ ndx )
3 5re 5 ∈ ℝ
4 5lt6 5 < 6
5 3 4 ltneii 5 ≠ 6
6 scandx ( Scalar ‘ ndx ) = 5
7 vscandx ( ·𝑠 ‘ ndx ) = 6
8 6 7 neeq12i ( ( Scalar ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ↔ 5 ≠ 6 )
9 5 8 mpbir ( Scalar ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
10 2 9 setsnid ( Scalar ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) = ( Scalar ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g𝐺 ) ⟩ ) )
11 zringring ring ∈ Ring
12 2 setsid ( ( 𝐺𝑉 ∧ ℤring ∈ Ring ) → ℤring = ( Scalar ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) )
13 11 12 mpan2 ( 𝐺𝑉 → ℤring = ( Scalar ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) )
14 eqid ( .g𝐺 ) = ( .g𝐺 )
15 1 14 zlmval ( 𝐺𝑉𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g𝐺 ) ⟩ ) )
16 15 fveq2d ( 𝐺𝑉 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g𝐺 ) ⟩ ) ) )
17 10 13 16 3eqtr4a ( 𝐺𝑉 → ℤring = ( Scalar ‘ 𝑊 ) )