# Metamath Proof Explorer

## Theorem zncrng

Description: Z/nZ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis zncrng.y 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
Assertion zncrng ( 𝑁 ∈ ℕ0𝑌 ∈ CRing )

### Proof

Step Hyp Ref Expression
1 zncrng.y 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
3 eqid ( RSpan ‘ ℤring ) = ( RSpan ‘ ℤring )
4 eqid ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) = ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
5 3 4 zncrng2 ( 𝑁 ∈ ℤ → ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ∈ CRing )
6 2 5 syl ( 𝑁 ∈ ℕ0 → ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ∈ CRing )
7 eqidd ( 𝑁 ∈ ℕ0 → ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) )
8 3 4 1 znbas2 ( 𝑁 ∈ ℕ0 → ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( Base ‘ 𝑌 ) )
9 3 4 1 znadd ( 𝑁 ∈ ℕ0 → ( +g ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( +g𝑌 ) )
10 9 oveqdr ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ) ) → ( 𝑥 ( +g ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) 𝑦 ) = ( 𝑥 ( +g𝑌 ) 𝑦 ) )
11 3 4 1 znmul ( 𝑁 ∈ ℕ0 → ( .r ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) = ( .r𝑌 ) )
12 11 oveqdr ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) ) ) → ( 𝑥 ( .r ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ) 𝑦 ) = ( 𝑥 ( .r𝑌 ) 𝑦 ) )
13 7 8 10 12 crngpropd ( 𝑁 ∈ ℕ0 → ( ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) ∈ CRing ↔ 𝑌 ∈ CRing ) )
14 6 13 mpbid ( 𝑁 ∈ ℕ0𝑌 ∈ CRing )