Metamath Proof Explorer

Theorem mndractfo

Description: An element X of a monoid E is right-invertible iff its right-translation G is surjective. (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses mndractfo.b 
|- B = ( Base ` E )
mndractfo.z 
|- .0. = ( 0g ` E )
mndractfo.p 
|- .+ = ( +g ` E )
mndractfo.f 
|- G = ( a e. B |-> ( a .+ X ) )
mndractfo.e 
|- ( ph -> E e. Mnd )
mndractfo.x 
|- ( ph -> X e. B )
Assertion mndractfo 
|- ( ph -> ( G : B -onto-> B <-> E. y e. B ( y .+ X ) = .0. ) )

Proof

Step Hyp Ref Expression
1 mndractfo.b 
 |-  B = ( Base ` E )
2 mndractfo.z 
 |-  .0. = ( 0g ` E )
3 mndractfo.p 
 |-  .+ = ( +g ` E )
4 mndractfo.f 
 |-  G = ( a e. B |-> ( a .+ X ) )
5 mndractfo.e 
 |-  ( ph -> E e. Mnd )
6 mndractfo.x 
 |-  ( ph -> X e. B )
7 simpr 
 |-  ( ( ph /\ G : B -onto-> B ) -> G : B -onto-> B )
8 1 2 mndidcl 
 |-  ( E e. Mnd -> .0. e. B )
9 5 8 syl 
 |-  ( ph -> .0. e. B )
10 9 adantr 
 |-  ( ( ph /\ G : B -onto-> B ) -> .0. e. B )
11 foelcdmi 
 |-  ( ( G : B -onto-> B /\ .0. e. B ) -> E. y e. B ( G ` y ) = .0. )
12 7 10 11 syl2anc 
 |-  ( ( ph /\ G : B -onto-> B ) -> E. y e. B ( G ` y ) = .0. )
13 oveq1 
 |-  ( a = y -> ( a .+ X ) = ( y .+ X ) )
14 simpr 
 |-  ( ( ( ph /\ G : B -onto-> B ) /\ y e. B ) -> y e. B )
15 ovexd 
 |-  ( ( ( ph /\ G : B -onto-> B ) /\ y e. B ) -> ( y .+ X ) e. _V )
16 4 13 14 15 fvmptd3 
 |-  ( ( ( ph /\ G : B -onto-> B ) /\ y e. B ) -> ( G ` y ) = ( y .+ X ) )
17 16 eqeq1d 
 |-  ( ( ( ph /\ G : B -onto-> B ) /\ y e. B ) -> ( ( G ` y ) = .0. <-> ( y .+ X ) = .0. ) )
18 17 biimpd 
 |-  ( ( ( ph /\ G : B -onto-> B ) /\ y e. B ) -> ( ( G ` y ) = .0. -> ( y .+ X ) = .0. ) )
19 18 reximdva 
 |-  ( ( ph /\ G : B -onto-> B ) -> ( E. y e. B ( G ` y ) = .0. -> E. y e. B ( y .+ X ) = .0. ) )
20 12 19 mpd 
 |-  ( ( ph /\ G : B -onto-> B ) -> E. y e. B ( y .+ X ) = .0. )
21 5 adantr 
 |-  ( ( ph /\ a e. B ) -> E e. Mnd )
22 simpr 
 |-  ( ( ph /\ a e. B ) -> a e. B )
23 6 adantr 
 |-  ( ( ph /\ a e. B ) -> X e. B )
24 1 3 21 22 23 mndcld 
 |-  ( ( ph /\ a e. B ) -> ( a .+ X ) e. B )
25 24 4 fmptd 
 |-  ( ph -> G : B --> B )
26 25 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) -> G : B --> B )
27 fveq2 
 |-  ( x = ( z .+ y ) -> ( G ` x ) = ( G ` ( z .+ y ) ) )
28 27 eqeq2d 
 |-  ( x = ( z .+ y ) -> ( z = ( G ` x ) <-> z = ( G ` ( z .+ y ) ) ) )
29 5 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> E e. Mnd )
30 simpr 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> z e. B )
31 simpllr 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> y e. B )
32 1 3 29 30 31 mndcld 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> ( z .+ y ) e. B )
33 6 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> X e. B )
34 1 3 29 30 31 33 mndassd 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> ( ( z .+ y ) .+ X ) = ( z .+ ( y .+ X ) ) )
35 oveq1 
 |-  ( a = ( z .+ y ) -> ( a .+ X ) = ( ( z .+ y ) .+ X ) )
36 ovexd 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> ( ( z .+ y ) .+ X ) e. _V )
37 4 35 32 36 fvmptd3 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> ( G ` ( z .+ y ) ) = ( ( z .+ y ) .+ X ) )
38 simplr 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> ( y .+ X ) = .0. )
39 38 oveq2d 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> ( z .+ ( y .+ X ) ) = ( z .+ .0. ) )
40 1 3 2 mndrid 
 |-  ( ( E e. Mnd /\ z e. B ) -> ( z .+ .0. ) = z )
41 29 30 40 syl2anc 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> ( z .+ .0. ) = z )
42 39 41 eqtr2d 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> z = ( z .+ ( y .+ X ) ) )
43 34 37 42 3eqtr4rd 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> z = ( G ` ( z .+ y ) ) )
44 28 32 43 rspcedvdw 
 |-  ( ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) /\ z e. B ) -> E. x e. B z = ( G ` x ) )
45 44 ralrimiva 
 |-  ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) -> A. z e. B E. x e. B z = ( G ` x ) )
46 dffo3 
 |-  ( G : B -onto-> B <-> ( G : B --> B /\ A. z e. B E. x e. B z = ( G ` x ) ) )
47 26 45 46 sylanbrc 
 |-  ( ( ( ph /\ y e. B ) /\ ( y .+ X ) = .0. ) -> G : B -onto-> B )
48 47 r19.29an 
 |-  ( ( ph /\ E. y e. B ( y .+ X ) = .0. ) -> G : B -onto-> B )
49 20 48 impbida 
 |-  ( ph -> ( G : B -onto-> B <-> E. y e. B ( y .+ X ) = .0. ) )