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. )