This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 mndlactfo.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
2 mndlactfo.z ⊢ 0 = ( 0g ‘ 𝐸 )
3 mndlactfo.p ⊢ + = ( +g ‘ 𝐸 )
4 mndlactfo.f ⊢ 𝐹 = ( 𝑎 ∈ 𝐵 ↦ ( 𝑋 + 𝑎 ) )
5 mndlactfo.e ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
6 mndlactfo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 mndlactf1.1 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 mndlactf1.2 ⊢ ( 𝜑 → ( 𝑌 + 𝑋 ) = 0 )
9 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐸 ∈ Mnd )
10 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
12 1 3 9 10 11 mndcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑋 + 𝑎 ) ∈ 𝐵 )
13 12 4 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐵 )
14 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) )
15 oveq2 ⊢ ( 𝑎 = 𝑖 → ( 𝑋 + 𝑎 ) = ( 𝑋 + 𝑖 ) )
16 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → 𝑖 ∈ 𝐵 )
17 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 𝑋 + 𝑖 ) ∈ V )
18 4 15 16 17 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑋 + 𝑖 ) )
19 oveq2 ⊢ ( 𝑎 = 𝑗 → ( 𝑋 + 𝑎 ) = ( 𝑋 + 𝑗 ) )
20 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → 𝑗 ∈ 𝐵 )
21 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 𝑋 + 𝑗 ) ∈ V )
22 4 19 20 21 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝑋 + 𝑗 ) )
23 14 18 22 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 𝑋 + 𝑖 ) = ( 𝑋 + 𝑗 ) )
24 23 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 𝑌 + ( 𝑋 + 𝑖 ) ) = ( 𝑌 + ( 𝑋 + 𝑗 ) ) )
25 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → 𝐸 ∈ Mnd )
26 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → 𝑌 ∈ 𝐵 )
27 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → 𝑋 ∈ 𝐵 )
28 1 3 25 26 27 16 mndassd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( ( 𝑌 + 𝑋 ) + 𝑖 ) = ( 𝑌 + ( 𝑋 + 𝑖 ) ) )
29 1 3 25 26 27 20 mndassd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( ( 𝑌 + 𝑋 ) + 𝑗 ) = ( 𝑌 + ( 𝑋 + 𝑗 ) ) )
30 24 28 29 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( ( 𝑌 + 𝑋 ) + 𝑖 ) = ( ( 𝑌 + 𝑋 ) + 𝑗 ) )
31 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 𝑌 + 𝑋 ) = 0 )
32 31 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( ( 𝑌 + 𝑋 ) + 𝑖 ) = ( 0 + 𝑖 ) )
33 31 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( ( 𝑌 + 𝑋 ) + 𝑗 ) = ( 0 + 𝑗 ) )
34 30 32 33 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 0 + 𝑖 ) = ( 0 + 𝑗 ) )
35 1 3 2 mndlid ⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑖 ∈ 𝐵 ) → ( 0 + 𝑖 ) = 𝑖 )
36 25 16 35 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) ∧ 𝑗 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) ) → ( 0 + 𝑖 ) = 𝑖 )
37 1 3 2 mndlid ⊢ ( ( 𝐸 ∈ 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→ 𝐵 )