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 ⊢ W = ℤMod ⁡ G
Assertion zlmsca ⊢ G ∈ V → ℤ ring = Scalar ⁡ W

Proof

Step Hyp Ref Expression
1 zlmbas.w ⊢ W = ℤMod ⁡ G
2 scaid ⊢ Scalar = Slot Scalar ⁡ ndx
3 vscandxnscandx ⊢ ⋅ ndx ≠ Scalar ⁡ ndx
4 3 necomi ⊢ Scalar ⁡ ndx ≠ ⋅ ndx
5 2 4 setsnid ⊢ Scalar ⁡ G sSet Scalar ⁡ ndx ℤ ring = Scalar ⁡ G sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ G
6 zringring ⊢ ℤ ring ∈ Ring
7 2 setsid ⊢ G ∈ V ∧ ℤ ring ∈ Ring → ℤ ring = Scalar ⁡ G sSet Scalar ⁡ ndx ℤ ring
8 6 7 mpan2 ⊢ G ∈ V → ℤ ring = Scalar ⁡ G sSet Scalar ⁡ ndx ℤ ring
9 eqid ⊢ ⋅ G = ⋅ G
10 1 9 zlmval ⊢ G ∈ V → W = G sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ G
11 10 fveq2d ⊢ G ∈ V → Scalar ⁡ W = Scalar ⁡ G sSet Scalar ⁡ ndx ℤ ring sSet ⋅ ndx ⋅ G
12 5 8 11 3eqtr4a ⊢ G ∈ V → ℤ ring = Scalar ⁡ W