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 )