# Metamath Proof Explorer

## Theorem zrhunitpreima

Description: The preimage by ZRHom of the unit of a division ring is ( ZZ \ { 0 } ) . (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Hypotheses zrhker.0
`|- B = ( Base ` R )`
zrhker.1
`|- L = ( ZRHom ` R )`
zrhker.2
`|- .0. = ( 0g ` R )`
Assertion zrhunitpreima
`|- ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( `' L " ( Unit ` R ) ) = ( ZZ \ { 0 } ) )`

### Proof

Step Hyp Ref Expression
1 zrhker.0
` |-  B = ( Base ` R )`
2 zrhker.1
` |-  L = ( ZRHom ` R )`
3 zrhker.2
` |-  .0. = ( 0g ` R )`
4 eqid
` |-  ( Unit ` R ) = ( Unit ` R )`
5 eqid
` |-  ( 0g ` R ) = ( 0g ` R )`
6 1 4 5 isdrng
` |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( B \ { ( 0g ` R ) } ) ) )`
7 6 simprbi
` |-  ( R e. DivRing -> ( Unit ` R ) = ( B \ { ( 0g ` R ) } ) )`
8 7 imaeq2d
` |-  ( R e. DivRing -> ( `' L " ( Unit ` R ) ) = ( `' L " ( B \ { ( 0g ` R ) } ) ) )`
` |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( `' L " ( Unit ` R ) ) = ( `' L " ( B \ { ( 0g ` R ) } ) ) )`
10 drngring
` |-  ( R e. DivRing -> R e. Ring )`
11 2 zrhrhm
` |-  ( R e. Ring -> L e. ( ZZring RingHom R ) )`
12 zringbas
` |-  ZZ = ( Base ` ZZring )`
13 12 1 rhmf
` |-  ( L e. ( ZZring RingHom R ) -> L : ZZ --> B )`
14 ffun
` |-  ( L : ZZ --> B -> Fun L )`
15 11 13 14 3syl
` |-  ( R e. Ring -> Fun L )`
16 difpreima
` |-  ( Fun L -> ( `' L " ( B \ { ( 0g ` R ) } ) ) = ( ( `' L " B ) \ ( `' L " { ( 0g ` R ) } ) ) )`
17 10 15 16 3syl
` |-  ( R e. DivRing -> ( `' L " ( B \ { ( 0g ` R ) } ) ) = ( ( `' L " B ) \ ( `' L " { ( 0g ` R ) } ) ) )`
` |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( `' L " ( B \ { ( 0g ` R ) } ) ) = ( ( `' L " B ) \ ( `' L " { ( 0g ` R ) } ) ) )`
19 fimacnv
` |-  ( L : ZZ --> B -> ( `' L " B ) = ZZ )`
20 10 11 13 19 4syl
` |-  ( R e. DivRing -> ( `' L " B ) = ZZ )`
` |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( `' L " B ) = ZZ )`
` |-  ( R e. Ring -> ( ( chr ` R ) = 0 <-> ( `' L " { ( 0g ` R ) } ) = { 0 } ) )`
` |-  ( ( R e. Ring /\ ( chr ` R ) = 0 ) -> ( `' L " { ( 0g ` R ) } ) = { 0 } )`
` |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( `' L " { ( 0g ` R ) } ) = { 0 } )`
` |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( `' L " B ) \ ( `' L " { ( 0g ` R ) } ) ) = ( ZZ \ { 0 } ) )`
` |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( `' L " ( Unit ` R ) ) = ( ZZ \ { 0 } ) )`