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

Metamath Proof Explorer

Theorem mndlrinvb

Description: In a monoid, if an element has both a left-inverse and a right-inverse, they are equal. (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses mndlrinv.b 
|- B = ( Base ` E )
mndlrinv.z 
|- .0. = ( 0g ` E )
mndlrinv.p 
|- .+ = ( +g ` E )
mndlrinv.e 
|- ( ph -> E e. Mnd )
mndlrinv.x 
|- ( ph -> X e. B )
Assertion mndlrinvb 
|- ( ph -> ( ( E. u e. B ( X .+ u ) = .0. /\ E. v e. B ( v .+ X ) = .0. ) <-> E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) )

Proof

Step Hyp Ref Expression
1 mndlrinv.b 
 |-  B = ( Base ` E )
2 mndlrinv.z 
 |-  .0. = ( 0g ` E )
3 mndlrinv.p 
 |-  .+ = ( +g ` E )
4 mndlrinv.e 
 |-  ( ph -> E e. Mnd )
5 mndlrinv.x 
 |-  ( ph -> X e. B )
6 oveq2 
 |-  ( z = u -> ( X .+ z ) = ( X .+ u ) )
7 6 eqeq1d 
 |-  ( z = u -> ( ( X .+ z ) = .0. <-> ( X .+ u ) = .0. ) )
8 oveq1 
 |-  ( z = u -> ( z .+ X ) = ( u .+ X ) )
9 8 eqeq1d 
 |-  ( z = u -> ( ( z .+ X ) = .0. <-> ( u .+ X ) = .0. ) )
10 7 9 anbi12d 
 |-  ( z = u -> ( ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) <-> ( ( X .+ u ) = .0. /\ ( u .+ X ) = .0. ) ) )
11 simplr 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> u e. B )
12 simpr 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( X .+ u ) = .0. )
13 4 ad4antr 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> E e. Mnd )
14 5 ad4antr 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> X e. B )
15 simpllr 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> v e. B )
16 simp-4r 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( v .+ X ) = .0. )
17 1 2 3 13 14 15 11 16 12 mndlrinv 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> v = u )
18 17 oveq1d 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( v .+ X ) = ( u .+ X ) )
19 18 16 eqtr3d 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( u .+ X ) = .0. )
20 12 19 jca 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( ( X .+ u ) = .0. /\ ( u .+ X ) = .0. ) )
21 10 11 20 rspcedvdw 
 |-  ( ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> E. z e. B ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) )
22 21 r19.29an 
 |-  ( ( ( ( ph /\ ( v .+ X ) = .0. ) /\ v e. B ) /\ E. u e. B ( X .+ u ) = .0. ) -> E. z e. B ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) )
23 22 an42ds 
 |-  ( ( ( ( ph /\ E. u e. B ( X .+ u ) = .0. ) /\ v e. B ) /\ ( v .+ X ) = .0. ) -> E. z e. B ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) )
24 23 r19.29an 
 |-  ( ( ( ph /\ E. u e. B ( X .+ u ) = .0. ) /\ E. v e. B ( v .+ X ) = .0. ) -> E. z e. B ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) )
25 24 anasss 
 |-  ( ( ph /\ ( E. u e. B ( X .+ u ) = .0. /\ E. v e. B ( v .+ X ) = .0. ) ) -> E. z e. B ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) )
26 oveq2 
 |-  ( u = z -> ( X .+ u ) = ( X .+ z ) )
27 26 eqeq1d 
 |-  ( u = z -> ( ( X .+ u ) = .0. <-> ( X .+ z ) = .0. ) )
28 simplr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) ) -> z e. B )
29 simprl 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) ) -> ( X .+ z ) = .0. )
30 27 28 29 rspcedvdw 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) ) -> E. u e. B ( X .+ u ) = .0. )
31 oveq1 
 |-  ( v = z -> ( v .+ X ) = ( z .+ X ) )
32 31 eqeq1d 
 |-  ( v = z -> ( ( v .+ X ) = .0. <-> ( z .+ X ) = .0. ) )
33 simprr 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) ) -> ( z .+ X ) = .0. )
34 32 28 33 rspcedvdw 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) ) -> E. v e. B ( v .+ X ) = .0. )
35 30 34 jca 
 |-  ( ( ( ph /\ z e. B ) /\ ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) ) -> ( E. u e. B ( X .+ u ) = .0. /\ E. v e. B ( v .+ X ) = .0. ) )
36 35 r19.29an 
 |-  ( ( ph /\ E. z e. B ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) ) -> ( E. u e. B ( X .+ u ) = .0. /\ E. v e. B ( v .+ X ) = .0. ) )
37 25 36 impbida 
 |-  ( ph -> ( ( E. u e. B ( X .+ u ) = .0. /\ E. v e. B ( v .+ X ) = .0. ) <-> E. z e. B ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) ) )
38 oveq2 
 |-  ( y = z -> ( X .+ y ) = ( X .+ z ) )
39 38 eqeq1d 
 |-  ( y = z -> ( ( X .+ y ) = .0. <-> ( X .+ z ) = .0. ) )
40 oveq1 
 |-  ( y = z -> ( y .+ X ) = ( z .+ X ) )
41 40 eqeq1d 
 |-  ( y = z -> ( ( y .+ X ) = .0. <-> ( z .+ X ) = .0. ) )
42 39 41 anbi12d 
 |-  ( y = z -> ( ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) <-> ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) ) )
43 42 cbvrexvw 
 |-  ( E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) <-> E. z e. B ( ( X .+ z ) = .0. /\ ( z .+ X ) = .0. ) )
44 37 43 bitr4di 
 |-  ( ph -> ( ( E. u e. B ( X .+ u ) = .0. /\ E. v e. B ( v .+ X ) = .0. ) <-> E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) )