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 | ⊢ 𝑆 = ( RSpan ‘ ℤring ) | |
znval.u | ⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) ) | ||
Assertion | zncrng2 | ⊢ ( 𝑁 ∈ ℤ → 𝑈 ∈ CRing ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | znval.s | ⊢ 𝑆 = ( RSpan ‘ ℤring ) | |
2 | znval.u | ⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) ) | |
3 | zringcrng | ⊢ ℤring ∈ CRing | |
4 | 1 | znlidl | ⊢ ( 𝑁 ∈ ℤ → ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) ) |
5 | eqid | ⊢ ( LIdeal ‘ ℤring ) = ( LIdeal ‘ ℤring ) | |
6 | 2 5 | quscrng | ⊢ ( ( ℤring ∈ CRing ∧ ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) ) → 𝑈 ∈ CRing ) |
7 | 3 4 6 | sylancr | ⊢ ( 𝑁 ∈ ℤ → 𝑈 ∈ CRing ) |