This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )