Theorem drnginvrn0

Description: The multiplicative inverse in a division ring is nonzero. ( recne0 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	drnginvrn0	|- ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( I ` X ) =/= .0. )

Proof

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