Description: The neutral element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017) (Revised by AV, 9-Jun-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | zring0 | |- 0 = ( 0g ` ZZring ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cncrng | |- CCfld e. CRing |
|
| 2 | crngring | |- ( CCfld e. CRing -> CCfld e. Ring ) |
|
| 3 | ringmnd | |- ( CCfld e. Ring -> CCfld e. Mnd ) |
|
| 4 | 1 2 3 | mp2b | |- CCfld e. Mnd |
| 5 | 0z | |- 0 e. ZZ |
|
| 6 | zsscn | |- ZZ C_ CC |
|
| 7 | df-zring | |- ZZring = ( CCfld |`s ZZ ) |
|
| 8 | cnfldbas | |- CC = ( Base ` CCfld ) |
|
| 9 | cnfld0 | |- 0 = ( 0g ` CCfld ) |
|
| 10 | 7 8 9 | ress0g | |- ( ( CCfld e. Mnd /\ 0 e. ZZ /\ ZZ C_ CC ) -> 0 = ( 0g ` ZZring ) ) |
| 11 | 4 5 6 10 | mp3an | |- 0 = ( 0g ` ZZring ) |