Metamath Proof Explorer

Theorem zncrng

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

Ref Expression
Hypothesis zncrng.y 
|- Y = ( Z/nZ ` N )
Assertion zncrng 
|- ( N e. NN0 -> Y e. CRing )

Proof

Step Hyp Ref Expression
1 zncrng.y 
 |-  Y = ( Z/nZ ` N )
2 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
3 eqid 
 |-  ( RSpan ` ZZring ) = ( RSpan ` ZZring )
4 eqid 
 |-  ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) = ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) )
5 3 4 zncrng2 
 |-  ( N e. ZZ -> ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) e. CRing )
6 2 5 syl 
 |-  ( N e. NN0 -> ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) e. CRing )
7 eqidd 
 |-  ( N e. NN0 -> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) )
8 3 4 1 znbas2 
 |-  ( N e. NN0 -> ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( Base ` Y ) )
9 3 4 1 znadd 
 |-  ( N e. NN0 -> ( +g ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( +g ` Y ) )
10 9 oveqdr 
 |-  ( ( N e. NN0 /\ ( x e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) /\ y e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) ) ) -> ( x ( +g ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) y ) = ( x ( +g ` Y ) y ) )
11 3 4 1 znmul 
 |-  ( N e. NN0 -> ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( .r ` Y ) )
12 11 oveqdr 
 |-  ( ( N e. NN0 /\ ( x e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) /\ y e. ( Base ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) ) ) -> ( x ( .r ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) y ) = ( x ( .r ` Y ) y ) )
13 7 8 10 12 crngpropd 
 |-  ( N e. NN0 -> ( ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) e. CRing <-> Y e. CRing ) )
14 6 13 mpbid 
 |-  ( N e. NN0 -> Y e. CRing )