This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ringinveu

Description: If a ring unit element X admits both a left inverse Y and a right inverse Z , they are equal. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses isdrng4.b 
|- B = ( Base ` R )
isdrng4.0 
|- .0. = ( 0g ` R )
isdrng4.1 
|- .1. = ( 1r ` R )
isdrng4.x 
|- .x. = ( .r ` R )
isdrng4.u 
|- U = ( Unit ` R )
isdrng4.r 
|- ( ph -> R e. Ring )
ringinveu.1 
|- ( ph -> X e. B )
ringinveu.2 
|- ( ph -> Y e. B )
ringinveu.3 
|- ( ph -> Z e. B )
ringinveu.4 
|- ( ph -> ( Y .x. X ) = .1. )
ringinveu.5 
|- ( ph -> ( X .x. Z ) = .1. )
Assertion ringinveu 
|- ( ph -> Z = Y )

Proof

Step Hyp Ref Expression
1 isdrng4.b 
 |-  B = ( Base ` R )
2 isdrng4.0 
 |-  .0. = ( 0g ` R )
3 isdrng4.1 
 |-  .1. = ( 1r ` R )
4 isdrng4.x 
 |-  .x. = ( .r ` R )
5 isdrng4.u 
 |-  U = ( Unit ` R )
6 isdrng4.r 
 |-  ( ph -> R e. Ring )
7 ringinveu.1 
 |-  ( ph -> X e. B )
8 ringinveu.2 
 |-  ( ph -> Y e. B )
9 ringinveu.3 
 |-  ( ph -> Z e. B )
10 ringinveu.4 
 |-  ( ph -> ( Y .x. X ) = .1. )
11 ringinveu.5 
 |-  ( ph -> ( X .x. Z ) = .1. )
12 11 oveq2d 
 |-  ( ph -> ( Y .x. ( X .x. Z ) ) = ( Y .x. .1. ) )
13 10 oveq1d 
 |-  ( ph -> ( ( Y .x. X ) .x. Z ) = ( .1. .x. Z ) )
14 1 4 6 8 7 9 ringassd 
 |-  ( ph -> ( ( Y .x. X ) .x. Z ) = ( Y .x. ( X .x. Z ) ) )
15 1 4 3 6 9 ringlidmd 
 |-  ( ph -> ( .1. .x. Z ) = Z )
16 13 14 15 3eqtr3d 
 |-  ( ph -> ( Y .x. ( X .x. Z ) ) = Z )
17 1 4 3 6 8 ringridmd 
 |-  ( ph -> ( Y .x. .1. ) = Y )
18 12 16 17 3eqtr3d 
 |-  ( ph -> Z = Y )