Metamath Proof Explorer

Theorem mndlactf1o

Description: An element X of a monoid E is invertible iff its left-translation F is bijective. See also grplactf1o . Remark in chapter I. of BourbakiAlg1 p. 17. (Contributed by Thierry Arnoux, 3-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 mndlactf1o.b 
 |-  B = ( Base ` E )
2 mndlactf1o.z 
 |-  .0. = ( 0g ` E )
3 mndlactf1o.p 
 |-  .+ = ( +g ` E )
4 mndlactf1o.f 
 |-  F = ( a e. B |-> ( X .+ a ) )
5 mndlactf1o.e 
 |-  ( ph -> E e. Mnd )
6 mndlactf1o.x 
 |-  ( ph -> X e. B )
7 oveq2 
 |-  ( y = u -> ( X .+ y ) = ( X .+ u ) )
8 7 eqeq1d 
 |-  ( y = u -> ( ( X .+ y ) = .0. <-> ( X .+ u ) = .0. ) )
9 oveq1 
 |-  ( y = u -> ( y .+ X ) = ( u .+ X ) )
10 9 eqeq1d 
 |-  ( y = u -> ( ( y .+ X ) = .0. <-> ( u .+ X ) = .0. ) )
11 8 10 anbi12d 
 |-  ( y = u -> ( ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) <-> ( ( X .+ u ) = .0. /\ ( u .+ X ) = .0. ) ) )
12 simplr 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> u e. B )
13 simpr 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( X .+ u ) = .0. )
14 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> E e. Mnd )
15 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> X e. B )
16 simp-4r 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> v e. B )
17 simpllr 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( v .+ X ) = .0. )
18 1 2 3 14 15 16 12 17 13 mndlrinv 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> v = u )
19 18 oveq1d 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( v .+ X ) = ( u .+ X ) )
20 19 17 eqtr3d 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( u .+ X ) = .0. )
21 13 20 jca 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> ( ( X .+ u ) = .0. /\ ( u .+ X ) = .0. ) )
22 11 12 21 rspcedvdw 
 |-  ( ( ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) /\ u e. B ) /\ ( X .+ u ) = .0. ) -> E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) )
23 f1ofo 
 |-  ( F : B -1-1-onto-> B -> F : B -onto-> B )
24 23 adantl 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> F : B -onto-> B )
25 1 2 3 4 5 6 mndlactfo 
 |-  ( ph -> ( F : B -onto-> B <-> E. u e. B ( X .+ u ) = .0. ) )
26 25 biimpa 
 |-  ( ( ph /\ F : B -onto-> B ) -> E. u e. B ( X .+ u ) = .0. )
27 24 26 syldan 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> E. u e. B ( X .+ u ) = .0. )
28 27 ad2antrr 
 |-  ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) -> E. u e. B ( X .+ u ) = .0. )
29 22 28 r19.29a 
 |-  ( ( ( ( ph /\ F : B -1-1-onto-> B ) /\ v e. B ) /\ ( v .+ X ) = .0. ) -> E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) )
30 oveq1 
 |-  ( v = ( `' F ` .0. ) -> ( v .+ X ) = ( ( `' F ` .0. ) .+ X ) )
31 30 eqeq1d 
 |-  ( v = ( `' F ` .0. ) -> ( ( v .+ X ) = .0. <-> ( ( `' F ` .0. ) .+ X ) = .0. ) )
32 f1ocnv 
 |-  ( F : B -1-1-onto-> B -> `' F : B -1-1-onto-> B )
33 f1of 
 |-  ( `' F : B -1-1-onto-> B -> `' F : B --> B )
34 32 33 syl 
 |-  ( F : B -1-1-onto-> B -> `' F : B --> B )
35 34 adantl 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> `' F : B --> B )
36 1 2 mndidcl 
 |-  ( E e. Mnd -> .0. e. B )
37 5 36 syl 
 |-  ( ph -> .0. e. B )
38 37 adantr 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> .0. e. B )
39 35 38 ffvelcdmd 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( `' F ` .0. ) e. B )
40 f1of1 
 |-  ( F : B -1-1-onto-> B -> F : B -1-1-> B )
41 40 adantl 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> F : B -1-1-> B )
42 5 adantr 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> E e. Mnd )
43 6 adantr 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> X e. B )
44 1 3 42 39 43 mndcld 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( ( `' F ` .0. ) .+ X ) e. B )
45 44 38 jca 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( ( ( `' F ` .0. ) .+ X ) e. B /\ .0. e. B ) )
46 1 3 2 mndrid 
 |-  ( ( E e. Mnd /\ X e. B ) -> ( X .+ .0. ) = X )
47 42 43 46 syl2anc 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( X .+ .0. ) = X )
48 oveq2 
 |-  ( a = .0. -> ( X .+ a ) = ( X .+ .0. ) )
49 ovexd 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( X .+ .0. ) e. _V )
50 4 48 38 49 fvmptd3 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( F ` .0. ) = ( X .+ .0. ) )
51 oveq2 
 |-  ( a = ( ( `' F ` .0. ) .+ X ) -> ( X .+ a ) = ( X .+ ( ( `' F ` .0. ) .+ X ) ) )
52 ovexd 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( X .+ ( ( `' F ` .0. ) .+ X ) ) e. _V )
53 4 51 44 52 fvmptd3 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( F ` ( ( `' F ` .0. ) .+ X ) ) = ( X .+ ( ( `' F ` .0. ) .+ X ) ) )
54 oveq2 
 |-  ( a = ( `' F ` .0. ) -> ( X .+ a ) = ( X .+ ( `' F ` .0. ) ) )
55 ovexd 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( X .+ ( `' F ` .0. ) ) e. _V )
56 4 54 39 55 fvmptd3 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( F ` ( `' F ` .0. ) ) = ( X .+ ( `' F ` .0. ) ) )
57 simpr 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> F : B -1-1-onto-> B )
58 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> B /\ .0. e. B ) -> ( F ` ( `' F ` .0. ) ) = .0. )
59 57 38 58 syl2anc 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( F ` ( `' F ` .0. ) ) = .0. )
60 56 59 eqtr3d 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( X .+ ( `' F ` .0. ) ) = .0. )
61 60 oveq1d 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( ( X .+ ( `' F ` .0. ) ) .+ X ) = ( .0. .+ X ) )
62 1 3 42 43 39 43 mndassd 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( ( X .+ ( `' F ` .0. ) ) .+ X ) = ( X .+ ( ( `' F ` .0. ) .+ X ) ) )
63 1 3 2 mndlid 
 |-  ( ( E e. Mnd /\ X e. B ) -> ( .0. .+ X ) = X )
64 42 43 63 syl2anc 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( .0. .+ X ) = X )
65 61 62 64 3eqtr3d 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( X .+ ( ( `' F ` .0. ) .+ X ) ) = X )
66 53 65 eqtrd 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( F ` ( ( `' F ` .0. ) .+ X ) ) = X )
67 47 50 66 3eqtr4rd 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( F ` ( ( `' F ` .0. ) .+ X ) ) = ( F ` .0. ) )
68 f1fveq 
 |-  ( ( F : B -1-1-> B /\ ( ( ( `' F ` .0. ) .+ X ) e. B /\ .0. e. B ) ) -> ( ( F ` ( ( `' F ` .0. ) .+ X ) ) = ( F ` .0. ) <-> ( ( `' F ` .0. ) .+ X ) = .0. ) )
69 68 biimpa 
 |-  ( ( ( F : B -1-1-> B /\ ( ( ( `' F ` .0. ) .+ X ) e. B /\ .0. e. B ) ) /\ ( F ` ( ( `' F ` .0. ) .+ X ) ) = ( F ` .0. ) ) -> ( ( `' F ` .0. ) .+ X ) = .0. )
70 41 45 67 69 syl21anc 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> ( ( `' F ` .0. ) .+ X ) = .0. )
71 31 39 70 rspcedvdw 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> E. v e. B ( v .+ X ) = .0. )
72 29 71 r19.29a 
 |-  ( ( ph /\ F : B -1-1-onto-> B ) -> E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) )
73 oveq1 
 |-  ( v = y -> ( v .+ X ) = ( y .+ X ) )
74 73 eqeq1d 
 |-  ( v = y -> ( ( v .+ X ) = .0. <-> ( y .+ X ) = .0. ) )
75 simplr 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) -> y e. B )
76 simprr 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) -> ( y .+ X ) = .0. )
77 74 75 76 rspcedvdw 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) -> E. v e. B ( v .+ X ) = .0. )
78 oveq2 
 |-  ( u = y -> ( X .+ u ) = ( X .+ y ) )
79 78 eqeq1d 
 |-  ( u = y -> ( ( X .+ u ) = .0. <-> ( X .+ y ) = .0. ) )
80 simprl 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) -> ( X .+ y ) = .0. )
81 79 75 80 rspcedvdw 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) -> E. u e. B ( X .+ u ) = .0. )
82 77 81 jca 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) -> ( E. v e. B ( v .+ X ) = .0. /\ E. u e. B ( X .+ u ) = .0. ) )
83 82 r19.29an 
 |-  ( ( ph /\ E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) -> ( E. v e. B ( v .+ X ) = .0. /\ E. u e. B ( X .+ u ) = .0. ) )
84 5 ad2antrr 
 |-  ( ( ( ph /\ v e. B ) /\ ( v .+ X ) = .0. ) -> E e. Mnd )
85 6 ad2antrr 
 |-  ( ( ( ph /\ v e. B ) /\ ( v .+ X ) = .0. ) -> X e. B )
86 simplr 
 |-  ( ( ( ph /\ v e. B ) /\ ( v .+ X ) = .0. ) -> v e. B )
87 simpr 
 |-  ( ( ( ph /\ v e. B ) /\ ( v .+ X ) = .0. ) -> ( v .+ X ) = .0. )
88 1 2 3 4 84 85 86 87 mndlactf1 
 |-  ( ( ( ph /\ v e. B ) /\ ( v .+ X ) = .0. ) -> F : B -1-1-> B )
89 88 r19.29an 
 |-  ( ( ph /\ E. v e. B ( v .+ X ) = .0. ) -> F : B -1-1-> B )
90 25 biimpar 
 |-  ( ( ph /\ E. u e. B ( X .+ u ) = .0. ) -> F : B -onto-> B )
91 89 90 anim12dan 
 |-  ( ( ph /\ ( E. v e. B ( v .+ X ) = .0. /\ E. u e. B ( X .+ u ) = .0. ) ) -> ( F : B -1-1-> B /\ F : B -onto-> B ) )
92 df-f1o 
 |-  ( F : B -1-1-onto-> B <-> ( F : B -1-1-> B /\ F : B -onto-> B ) )
93 91 92 sylibr 
 |-  ( ( ph /\ ( E. v e. B ( v .+ X ) = .0. /\ E. u e. B ( X .+ u ) = .0. ) ) -> F : B -1-1-onto-> B )
94 83 93 syldan 
 |-  ( ( ph /\ E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) -> F : B -1-1-onto-> B )
95 72 94 impbida 
 |-  ( ph -> ( F : B -1-1-onto-> B <-> E. y e. B ( ( X .+ y ) = .0. /\ ( y .+ X ) = .0. ) ) )