Metamath Proof Explorer

Theorem mndlactf1

Description: If an element X of a monoid E is right-invertible, with inverse Y , then its left-translation F is injective. See also grplactf1o . Remark in chapter I. of BourbakiAlg1 p. 17 . (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 )
mndlactf1.1 
|- ( ph -> Y e. B )
mndlactf1.2 
|- ( ph -> ( Y .+ X ) = .0. )
Assertion mndlactf1 
|- ( ph -> F : B -1-1-> B )

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 mndlactf1.1 
 |-  ( ph -> Y e. B )
8 mndlactf1.2 
 |-  ( ph -> ( Y .+ X ) = .0. )
9 5 adantr 
 |-  ( ( ph /\ a e. B ) -> E e. Mnd )
10 6 adantr 
 |-  ( ( ph /\ a e. B ) -> X e. B )
11 simpr 
 |-  ( ( ph /\ a e. B ) -> a e. B )
12 1 3 9 10 11 mndcld 
 |-  ( ( ph /\ a e. B ) -> ( X .+ a ) e. B )
13 12 4 fmptd 
 |-  ( ph -> F : B --> B )
14 simpr 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( F ` i ) = ( F ` j ) )
15 oveq2 
 |-  ( a = i -> ( X .+ a ) = ( X .+ i ) )
16 simpllr 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> i e. B )
17 ovexd 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( X .+ i ) e. _V )
18 4 15 16 17 fvmptd3 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( F ` i ) = ( X .+ i ) )
19 oveq2 
 |-  ( a = j -> ( X .+ a ) = ( X .+ j ) )
20 simplr 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> j e. B )
21 ovexd 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( X .+ j ) e. _V )
22 4 19 20 21 fvmptd3 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( F ` j ) = ( X .+ j ) )
23 14 18 22 3eqtr3d 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( X .+ i ) = ( X .+ j ) )
24 23 oveq2d 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( Y .+ ( X .+ i ) ) = ( Y .+ ( X .+ j ) ) )
25 5 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> E e. Mnd )
26 7 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> Y e. B )
27 6 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> X e. B )
28 1 3 25 26 27 16 mndassd 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( ( Y .+ X ) .+ i ) = ( Y .+ ( X .+ i ) ) )
29 1 3 25 26 27 20 mndassd 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( ( Y .+ X ) .+ j ) = ( Y .+ ( X .+ j ) ) )
30 24 28 29 3eqtr4d 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( ( Y .+ X ) .+ i ) = ( ( Y .+ X ) .+ j ) )
31 8 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( Y .+ X ) = .0. )
32 31 oveq1d 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( ( Y .+ X ) .+ i ) = ( .0. .+ i ) )
33 31 oveq1d 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( ( Y .+ X ) .+ j ) = ( .0. .+ j ) )
34 30 32 33 3eqtr3d 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( .0. .+ i ) = ( .0. .+ j ) )
35 1 3 2 mndlid 
 |-  ( ( E e. Mnd /\ i e. B ) -> ( .0. .+ i ) = i )
36 25 16 35 syl2anc 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( .0. .+ i ) = i )
37 1 3 2 mndlid 
 |-  ( ( E e. Mnd /\ j e. B ) -> ( .0. .+ j ) = j )
38 25 20 37 syl2anc 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> ( .0. .+ j ) = j )
39 34 36 38 3eqtr3d 
 |-  ( ( ( ( ph /\ i e. B ) /\ j e. B ) /\ ( F ` i ) = ( F ` j ) ) -> i = j )
40 39 ex 
 |-  ( ( ( ph /\ i e. B ) /\ j e. B ) -> ( ( F ` i ) = ( F ` j ) -> i = j ) )
41 40 anasss 
 |-  ( ( ph /\ ( i e. B /\ j e. B ) ) -> ( ( F ` i ) = ( F ` j ) -> i = j ) )
42 41 ralrimivva 
 |-  ( ph -> A. i e. B A. j e. B ( ( F ` i ) = ( F ` j ) -> i = j ) )
43 dff13 
 |-  ( F : B -1-1-> B <-> ( F : B --> B /\ A. i e. B A. j e. B ( ( F ` i ) = ( F ` j ) -> i = j ) ) )
44 13 42 43 sylanbrc 
 |-  ( ph -> F : B -1-1-> B )