Metamath Proof Explorer


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