Theorem drnginvrld

Description: Property of the multiplicative inverse in a division ring. ( recid2d 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	drnginvrld	|- ( ph -> ( ( I ` X ) .x. 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	drnginvrl	|- ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( ( I ` X ) .x. X ) = .1. )
10	6 7 8 9	syl3anc	|- ( ph -> ( ( I ` X ) .x. X ) = .1. )