Metamath Proof Explorer

Theorem mndlactfo

Description: An element X of a monoid E is left-invertible iff its left-translation F is surjective. See also grplactf1o . (Contributed by Thierry Arnoux, 3-Aug-2025)

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

Proof

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