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 ⊢ 𝐵 = ( Base ‘ 𝐸 )
mndractfo.z ⊢ 0 = ( 0g ‘ 𝐸 )
mndractfo.p ⊢ + = ( +g ‘ 𝐸 )
mndractfo.f ⊢ 𝐺 = ( 𝑎 ∈ 𝐵 ↦ ( 𝑎 + 𝑋 ) )
mndractfo.e ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
mndractfo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mndractf1.1 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
mndractf1.2 ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = 0 )
Assertion mndractf1 ( 𝜑 → 𝐺 : 𝐵 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 mndractfo.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
2 mndractfo.z ⊢ 0 = ( 0g ‘ 𝐸 )
3 mndractfo.p ⊢ + = ( +g ‘ 𝐸 )
4 mndractfo.f ⊢ 𝐺 = ( 𝑎 ∈ 𝐵 ↦ ( 𝑎 + 𝑋 ) )
5 mndractfo.e ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
6 mndractfo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 mndractf1.1 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 mndractf1.2 ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = 0 )
9 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐸 ∈ Mnd )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
11 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12 1 3 9 10 11 mndcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 + 𝑋 ) ∈ 𝐵 )
13 12 4 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐵 )
14 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) )
15 oveq1 ⊢ ( 𝑎 = 𝑖 → ( 𝑎 + 𝑋 ) = ( 𝑖 + 𝑋 ) )
16 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → 𝑖 ∈ 𝐵 )
17 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑖 + 𝑋 ) ∈ V )
18 4 15 16 17 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝐺 ‘ 𝑖 ) = ( 𝑖 + 𝑋 ) )
19 oveq1 ⊢ ( 𝑎 = 𝑗 → ( 𝑎 + 𝑋 ) = ( 𝑗 + 𝑋 ) )
20 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → 𝑗 ∈ 𝐵 )
21 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑗 + 𝑋 ) ∈ V )
22 4 19 20 21 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝐺 ‘ 𝑗 ) = ( 𝑗 + 𝑋 ) )
23 14 18 22 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑖 + 𝑋 ) = ( 𝑗 + 𝑋 ) )
24 23 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( ( 𝑖 + 𝑋 ) + 𝑌 ) = ( ( 𝑗 + 𝑋 ) + 𝑌 ) )
25 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → 𝐸 ∈ Mnd )
26 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → 𝑋 ∈ 𝐵 )
27 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → 𝑌 ∈ 𝐵 )
28 1 3 25 16 26 27 mndassd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( ( 𝑖 + 𝑋 ) + 𝑌 ) = ( 𝑖 + ( 𝑋 + 𝑌 ) ) )
29 1 3 25 20 26 27 mndassd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( ( 𝑗 + 𝑋 ) + 𝑌 ) = ( 𝑗 + ( 𝑋 + 𝑌 ) ) )
30 24 28 29 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑖 + ( 𝑋 + 𝑌 ) ) = ( 𝑗 + ( 𝑋 + 𝑌 ) ) )
31 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑋 + 𝑌 ) = 0 )
32 31 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑖 + ( 𝑋 + 𝑌 ) ) = ( 𝑖 + 0 ) )
33 31 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑗 + ( 𝑋 + 𝑌 ) ) = ( 𝑗 + 0 ) )
34 30 32 33 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑖 + 0 ) = ( 𝑗 + 0 ) )
35 1 3 2 mndrid ⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑖 ∈ 𝐵 ) → ( 𝑖 + 0 ) = 𝑖 )
36 25 16 35 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑖 + 0 ) = 𝑖 )
37 1 3 2 mndrid ⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑗 ∈ 𝐵 ) → ( 𝑗 + 0 ) = 𝑗 )
38 25 20 37 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → ( 𝑗 + 0 ) = 𝑗 )
39 34 36 38 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ) → 𝑖 = 𝑗 )
40 39 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
41 40 anasss ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) ) → ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
42 41 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐵 ∀ 𝑗 ∈ 𝐵 ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
43 dff13 ⊢ ( 𝐺 : 𝐵 –1-1→ 𝐵 ↔ ( 𝐺 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑖 ∈ 𝐵 ∀ 𝑗 ∈ 𝐵 ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
44 13 42 43 sylanbrc ⊢ ( 𝜑 → 𝐺 : 𝐵 –1-1→ 𝐵 )