# Metamath Proof Explorer

## Theorem drnginvrcl

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

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

### Proof

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