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	⊢ 𝑆 = ( RSpan ‘ ℤring )
	znval2.u	⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
	znval2.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
Assertion	znmul	⊢ ( 𝑁 ∈ ℕ0 → ( .r ‘ 𝑈 ) = ( .r ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		znval2.s	⊢ 𝑆 = ( RSpan ‘ ℤring )
2		znval2.u	⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
3		znval2.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4		mulridx	⊢ .r = Slot ( .r ‘ ndx )
5		plendxnmulrndx	⊢ ( le ‘ ndx ) ≠ ( .r ‘ ndx )
6	5	necomi	⊢ ( .r ‘ ndx ) ≠ ( le ‘ ndx )
7	1 2 3 4 6	znbaslem	⊢ ( 𝑁 ∈ ℕ0 → ( .r ‘ 𝑈 ) = ( .r ‘ 𝑌 ) )