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