Metamath Proof Explorer

Theorem mndmolinv

Description: An element of a monoid that has a right inverse has at most one left inverse. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses mndmolinv.1 
|- B = ( Base ` M )
mndmolinv.2 
|- ( ph -> M e. Mnd )
mndmolinv.3 
|- ( ph -> A e. B )
mndmolinv.4 
|- ( ph -> E. x e. B ( A ( +g ` M ) x ) = ( 0g ` M ) )
Assertion mndmolinv 
|- ( ph -> E* x e. B ( x ( +g ` M ) A ) = ( 0g ` M ) )

Proof

Step Hyp Ref Expression
1 mndmolinv.1 
 |-  B = ( Base ` M )
2 mndmolinv.2 
 |-  ( ph -> M e. Mnd )
3 mndmolinv.3 
 |-  ( ph -> A e. B )
4 mndmolinv.4 
 |-  ( ph -> E. x e. B ( A ( +g ` M ) x ) = ( 0g ` M ) )
5 nfv 
 |-  F/ y ( A ( +g ` M ) x ) = ( 0g ` M )
6 nfv 
 |-  F/ x ( A ( +g ` M ) y ) = ( 0g ` M )
7 oveq2 
 |-  ( x = y -> ( A ( +g ` M ) x ) = ( A ( +g ` M ) y ) )
8 7 eqeq1d 
 |-  ( x = y -> ( ( A ( +g ` M ) x ) = ( 0g ` M ) <-> ( A ( +g ` M ) y ) = ( 0g ` M ) ) )
9 5 6 8 cbvrexw 
 |-  ( E. x e. B ( A ( +g ` M ) x ) = ( 0g ` M ) <-> E. y e. B ( A ( +g ` M ) y ) = ( 0g ` M ) )
10 9 biimpi 
 |-  ( E. x e. B ( A ( +g ` M ) x ) = ( 0g ` M ) -> E. y e. B ( A ( +g ` M ) y ) = ( 0g ` M ) )
11 4 10 syl 
 |-  ( ph -> E. y e. B ( A ( +g ` M ) y ) = ( 0g ` M ) )
12 2 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> M e. Mnd )
13 simplr 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> x e. B )
14 eqid 
 |-  ( +g ` M ) = ( +g ` M )
15 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
16 1 14 15 mndrid 
 |-  ( ( M e. Mnd /\ x e. B ) -> ( x ( +g ` M ) ( 0g ` M ) ) = x )
17 12 13 16 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( x ( +g ` M ) ( 0g ` M ) ) = x )
18 17 eqcomd 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> x = ( x ( +g ` M ) ( 0g ` M ) ) )
19 simpllr 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( A ( +g ` M ) y ) = ( 0g ` M ) )
20 19 eqcomd 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( 0g ` M ) = ( A ( +g ` M ) y ) )
21 20 oveq2d 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( x ( +g ` M ) ( 0g ` M ) ) = ( x ( +g ` M ) ( A ( +g ` M ) y ) ) )
22 18 21 eqtrd 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> x = ( x ( +g ` M ) ( A ( +g ` M ) y ) ) )
23 3 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> A e. B )
24 simp-4r 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> y e. B )
25 13 23 24 3jca 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( x e. B /\ A e. B /\ y e. B ) )
26 1 14 mndass 
 |-  ( ( M e. Mnd /\ ( x e. B /\ A e. B /\ y e. B ) ) -> ( ( x ( +g ` M ) A ) ( +g ` M ) y ) = ( x ( +g ` M ) ( A ( +g ` M ) y ) ) )
27 12 25 26 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( ( x ( +g ` M ) A ) ( +g ` M ) y ) = ( x ( +g ` M ) ( A ( +g ` M ) y ) ) )
28 27 eqcomd 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( x ( +g ` M ) ( A ( +g ` M ) y ) ) = ( ( x ( +g ` M ) A ) ( +g ` M ) y ) )
29 simpr 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( x ( +g ` M ) A ) = ( 0g ` M ) )
30 29 oveq1d 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( ( x ( +g ` M ) A ) ( +g ` M ) y ) = ( ( 0g ` M ) ( +g ` M ) y ) )
31 1 14 15 mndlid 
 |-  ( ( M e. Mnd /\ y e. B ) -> ( ( 0g ` M ) ( +g ` M ) y ) = y )
32 12 24 31 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( ( 0g ` M ) ( +g ` M ) y ) = y )
33 30 32 eqtrd 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> ( ( x ( +g ` M ) A ) ( +g ` M ) y ) = y )
34 22 28 33 3eqtrd 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) /\ ( x ( +g ` M ) A ) = ( 0g ` M ) ) -> x = y )
35 34 ex 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) /\ x e. B ) -> ( ( x ( +g ` M ) A ) = ( 0g ` M ) -> x = y ) )
36 35 ralrimiva 
 |-  ( ( ( ph /\ y e. B ) /\ ( A ( +g ` M ) y ) = ( 0g ` M ) ) -> A. x e. B ( ( x ( +g ` M ) A ) = ( 0g ` M ) -> x = y ) )
37 36 ex 
 |-  ( ( ph /\ y e. B ) -> ( ( A ( +g ` M ) y ) = ( 0g ` M ) -> A. x e. B ( ( x ( +g ` M ) A ) = ( 0g ` M ) -> x = y ) ) )
38 37 reximdva 
 |-  ( ph -> ( E. y e. B ( A ( +g ` M ) y ) = ( 0g ` M ) -> E. y e. B A. x e. B ( ( x ( +g ` M ) A ) = ( 0g ` M ) -> x = y ) ) )
39 11 38 mpd 
 |-  ( ph -> E. y e. B A. x e. B ( ( x ( +g ` M ) A ) = ( 0g ` M ) -> x = y ) )
40 nfv 
 |-  F/ y ( x ( +g ` M ) A ) = ( 0g ` M )
41 40 rmo2i 
 |-  ( E. y e. B A. x e. B ( ( x ( +g ` M ) A ) = ( 0g ` M ) -> x = y ) -> E* x e. B ( x ( +g ` M ) A ) = ( 0g ` M ) )
42 39 41 syl 
 |-  ( ph -> E* x e. B ( x ( +g ` M ) A ) = ( 0g ` M ) )