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 ‘ 𝑊 ) )