Theorem zlmbas

Description: Base set of a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 3-Nov-2024)

	Ref	Expression
Hypotheses	zlmbas.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
	zlmbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	zlmbas	⊢ 𝐵 = ( Base ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2		zlmbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		baseid	⊢ Base = Slot ( Base ‘ ndx )
4		scandxnbasendx	⊢ ( Scalar ‘ ndx ) ≠ ( Base ‘ ndx )
5	4	necomi	⊢ ( Base ‘ ndx ) ≠ ( Scalar ‘ ndx )
6		vscandxnbasendx	⊢ ( ·𝑠 ‘ ndx ) ≠ ( Base ‘ ndx )
7	6	necomi	⊢ ( Base ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
8	1 3 5 7	zlmlem	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 )
9	2 8	eqtri	⊢ 𝐵 = ( Base ‘ 𝑊 )