Metamath Proof Explorer


Theorem znmul

Description: The multiplicative structure of Z/nZ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019) (Revised by AV, 3-Nov-2024)

Ref Expression
Hypotheses znval2.s S=RSpanring
znval2.u U=ring/𝑠ring~QGSN
znval2.y Y=/N
Assertion znmul N0U=Y

Proof

Step Hyp Ref Expression
1 znval2.s S=RSpanring
2 znval2.u U=ring/𝑠ring~QGSN
3 znval2.y Y=/N
4 mulrid 𝑟=Slotndx
5 plendxnmulrndx ndxndx
6 5 necomi ndxndx
7 1 2 3 4 6 znbaslem N0U=Y