Description: The kernel of the homomorphism from the integers to a ring, if it is injective. (Contributed by Thierry Arnoux, 26-Oct-2017) (Revised by Thierry Arnoux, 23-May-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | zrhker.0 | |- B = ( Base ` R ) |
|
| zrhker.1 | |- L = ( ZRHom ` R ) |
||
| zrhker.2 | |- .0. = ( 0g ` R ) |
||
| Assertion | zrhf1ker | |- ( R e. Ring -> ( L : ZZ -1-1-> B <-> ( `' L " { .0. } ) = { 0 } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zrhker.0 | |- B = ( Base ` R ) |
|
| 2 | zrhker.1 | |- L = ( ZRHom ` R ) |
|
| 3 | zrhker.2 | |- .0. = ( 0g ` R ) |
|
| 4 | 2 | zrhrhm | |- ( R e. Ring -> L e. ( ZZring RingHom R ) ) |
| 5 | rhmghm | |- ( L e. ( ZZring RingHom R ) -> L e. ( ZZring GrpHom R ) ) |
|
| 6 | zringbas | |- ZZ = ( Base ` ZZring ) |
|
| 7 | zring0 | |- 0 = ( 0g ` ZZring ) |
|
| 8 | 6 1 7 3 | kerf1ghm | |- ( L e. ( ZZring GrpHom R ) -> ( L : ZZ -1-1-> B <-> ( `' L " { .0. } ) = { 0 } ) ) |
| 9 | 4 5 8 | 3syl | |- ( R e. Ring -> ( L : ZZ -1-1-> B <-> ( `' L " { .0. } ) = { 0 } ) ) |