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 )