This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) (Proof shortened by AV, 2-Nov-2024)

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 vscandxnscandx ⊢ ( ·𝑠 ‘ ndx ) ≠ ( Scalar ‘ ndx )
4 3 necomi ⊢ ( Scalar ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
5 2 4 setsnid ⊢ ( Scalar ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) = ( Scalar ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
6 zringring ⊢ ℤring ∈ Ring
7 2 setsid ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ℤring ∈ Ring ) → ℤring = ( Scalar ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) )
8 6 7 mpan2 ⊢ ( 𝐺 ∈ 𝑉 → ℤring = ( Scalar ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) )
9 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
10 1 9 zlmval ⊢ ( 𝐺 ∈ 𝑉 → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
11 10 fveq2d ⊢ ( 𝐺 ∈ 𝑉 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) ) )
12 5 8 11 3eqtr4a ⊢ ( 𝐺 ∈ 𝑉 → ℤring = ( Scalar ‘ 𝑊 ) )