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 ) |
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 ) |