Metamath Proof Explorer


Theorem zncrng2

Description: Making a commutative ring as a quotient of ZZ and n ZZ . (Contributed by Mario Carneiro, 12-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znval.s
|- S = ( RSpan ` ZZring )
znval.u
|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
Assertion zncrng2
|- ( N e. ZZ -> U e. CRing )

Proof

Step Hyp Ref Expression
1 znval.s
 |-  S = ( RSpan ` ZZring )
2 znval.u
 |-  U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
3 zringcrng
 |-  ZZring e. CRing
4 1 znlidl
 |-  ( N e. ZZ -> ( S ` { N } ) e. ( LIdeal ` ZZring ) )
5 eqid
 |-  ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
6 2 5 quscrng
 |-  ( ( ZZring e. CRing /\ ( S ` { N } ) e. ( LIdeal ` ZZring ) ) -> U e. CRing )
7 3 4 6 sylancr
 |-  ( N e. ZZ -> U e. CRing )