This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem drnginvrn0

Description: The multiplicative inverse in a division ring is nonzero. ( recne0 analog). (Contributed by NM, 19-Apr-2014)

Ref Expression
Hypotheses drnginvrcl.b 
|- B = ( Base ` R )
drnginvrcl.z 
|- .0. = ( 0g ` R )
drnginvrcl.i 
|- I = ( invr ` R )
Assertion drnginvrn0 
|- ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( I ` X ) =/= .0. )

Proof

Step Hyp Ref Expression
1 drnginvrcl.b 
 |-  B = ( Base ` R )
2 drnginvrcl.z 
 |-  .0. = ( 0g ` R )
3 drnginvrcl.i 
 |-  I = ( invr ` R )
4 drngring 
 |-  ( R e. DivRing -> R e. Ring )
5 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
6 5 3 unitinvcl 
 |-  ( ( R e. Ring /\ X e. ( Unit ` R ) ) -> ( I ` X ) e. ( Unit ` R ) )
7 6 ex 
 |-  ( R e. Ring -> ( X e. ( Unit ` R ) -> ( I ` X ) e. ( Unit ` R ) ) )
8 4 7 syl 
 |-  ( R e. DivRing -> ( X e. ( Unit ` R ) -> ( I ` X ) e. ( Unit ` R ) ) )
9 1 5 2 drngunit 
 |-  ( R e. DivRing -> ( X e. ( Unit ` R ) <-> ( X e. B /\ X =/= .0. ) ) )
10 1 5 2 drngunit 
 |-  ( R e. DivRing -> ( ( I ` X ) e. ( Unit ` R ) <-> ( ( I ` X ) e. B /\ ( I ` X ) =/= .0. ) ) )
11 8 9 10 3imtr3d 
 |-  ( R e. DivRing -> ( ( X e. B /\ X =/= .0. ) -> ( ( I ` X ) e. B /\ ( I ` X ) =/= .0. ) ) )
12 11 3impib 
 |-  ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( ( I ` X ) e. B /\ ( I ` X ) =/= .0. ) )
13 12 simprd 
 |-  ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( I ` X ) =/= .0. )