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 ring
znval.u U = ring / 𝑠 ring ~ QG S N
Assertion zncrng2 N U CRing

Proof

Step Hyp Ref Expression
1 znval.s S = RSpan ring
2 znval.u U = ring / 𝑠 ring ~ QG S N
3 zringcrng ring CRing
4 1 znlidl N S N LIdeal ring
5 eqid LIdeal ring = LIdeal ring
6 2 5 quscrng ring CRing S N LIdeal ring U CRing
7 3 4 6 sylancr N U CRing