Metamath Proof Explorer


Theorem drnginvrr

Description: Property of the multiplicative inverse in a division ring. ( recid analog). (Contributed by NM, 19-Apr-2014)

Ref Expression
Hypotheses drnginvrl.b
|- B = ( Base ` R )
drnginvrl.z
|- .0. = ( 0g ` R )
drnginvrl.t
|- .x. = ( .r ` R )
drnginvrl.u
|- .1. = ( 1r ` R )
drnginvrl.i
|- I = ( invr ` R )
Assertion drnginvrr
|- ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( X .x. ( I ` X ) ) = .1. )

Proof

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