# Metamath Proof Explorer

## Theorem drnginvrl

Description: Property of the multiplicative inverse in a division ring. ( recid2 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 drnginvrl
`|- ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( ( I ` X ) .x. 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 unitlinv
` |-  ( ( R e. Ring /\ X e. ( Unit ` R ) ) -> ( ( I ` X ) .x. X ) = .1. )`
10 9 ex
` |-  ( R e. Ring -> ( X e. ( Unit ` R ) -> ( ( I ` X ) .x. X ) = .1. ) )`
11 8 10 syl
` |-  ( R e. DivRing -> ( X e. ( Unit ` R ) -> ( ( I ` X ) .x. X ) = .1. ) )`
12 7 11 sylbird
` |-  ( R e. DivRing -> ( ( X e. B /\ X =/= .0. ) -> ( ( I ` X ) .x. X ) = .1. ) )`
13 12 3impib
` |-  ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( ( I ` X ) .x. X ) = .1. )`