Metamath Proof Explorer

Theorem mndractf1

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

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