Theorem drnginvrrd

Description: Property of the multiplicative inverse in a division ring. ( recidd analog). (Contributed by SN, 14-Aug-2024)

	Ref	Expression
Hypotheses	drnginvrld.b	|- B = ( Base ` R )
	drnginvrld.0	|- .0. = ( 0g ` R )
	drnginvrld.t	|- .x. = ( .r ` R )
	drnginvrld.u	|- .1. = ( 1r ` R )
	drnginvrld.i	|- I = ( invr ` R )
	drnginvrld.r	|- ( ph -> R e. DivRing )
	drnginvrld.x	|- ( ph -> X e. B )
	drnginvrld.1	|- ( ph -> X =/= .0. )
Assertion	drnginvrrd	|- ( ph -> ( X .x. ( I ` X ) ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		drnginvrld.b	|- B = ( Base ` R )
2		drnginvrld.0	|- .0. = ( 0g ` R )
3		drnginvrld.t	|- .x. = ( .r ` R )
4		drnginvrld.u	|- .1. = ( 1r ` R )
5		drnginvrld.i	|- I = ( invr ` R )
6		drnginvrld.r	|- ( ph -> R e. DivRing )
7		drnginvrld.x	|- ( ph -> X e. B )
8		drnginvrld.1	|- ( ph -> X =/= .0. )
9	1 2 3 4 5	drnginvrr	|- ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( X .x. ( I ` X ) ) = .1. )
10	6 7 8 9	syl3anc	|- ( ph -> ( X .x. ( I ` X ) ) = .1. )