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 )