Metamath Proof Explorer

Theorem elzrhunit

Description: Condition for the image by ZRHom to be a unit. (Contributed by Thierry Arnoux, 30-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 zrhker.0 
 |-  B = ( Base ` R )
2 zrhker.1 
 |-  L = ( ZRHom ` R )
3 zrhker.2 
 |-  .0. = ( 0g ` R )
4 simpll 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> R e. DivRing )
5 drngring 
 |-  ( R e. DivRing -> R e. Ring )
6 2 zrhrhm 
 |-  ( R e. Ring -> L e. ( ZZring RingHom R ) )
7 zringbas 
 |-  ZZ = ( Base ` ZZring )
8 7 1 rhmf 
 |-  ( L e. ( ZZring RingHom R ) -> L : ZZ --> B )
9 ffn 
 |-  ( L : ZZ --> B -> L Fn ZZ )
10 6 8 9 3syl 
 |-  ( R e. Ring -> L Fn ZZ )
11 4 5 10 3syl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> L Fn ZZ )
12 simprl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> M e. ZZ )
13 elsng 
 |-  ( M e. ZZ -> ( M e. { 0 } <-> M = 0 ) )
14 13 necon3bbid 
 |-  ( M e. ZZ -> ( -. M e. { 0 } <-> M =/= 0 ) )
15 14 biimpar 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> -. M e. { 0 } )
16 15 adantl 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> -. M e. { 0 } )
17 12 16 eldifd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> M e. ( ZZ \ { 0 } ) )
18 1 2 3 zrhunitpreima 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( `' L " ( Unit ` R ) ) = ( ZZ \ { 0 } ) )
19 18 adantr 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> ( `' L " ( Unit ` R ) ) = ( ZZ \ { 0 } ) )
20 17 19 eleqtrrd 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> M e. ( `' L " ( Unit ` R ) ) )
21 elpreima 
 |-  ( L Fn ZZ -> ( M e. ( `' L " ( Unit ` R ) ) <-> ( M e. ZZ /\ ( L ` M ) e. ( Unit ` R ) ) ) )
22 21 simplbda 
 |-  ( ( L Fn ZZ /\ M e. ( `' L " ( Unit ` R ) ) ) -> ( L ` M ) e. ( Unit ` R ) )
23 11 20 22 syl2anc 
 |-  ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> ( L ` M ) e. ( Unit ` R ) )