Metamath Proof Explorer

Theorem mndractfo

Description: An element X of a monoid E is right-invertible iff its right-translation G is surjective. (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 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion mndractfo ( 𝜑 → ( 𝐺 : 𝐵 –onto→ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) )

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 simpr ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) → 𝐺 : 𝐵 –onto→ 𝐵 )
8 1 2 mndidcl ⊢ ( 𝐸 ∈ Mnd → 0 ∈ 𝐵 )
9 5 8 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) → 0 ∈ 𝐵 )
11 foelcdmi ⊢ ( ( 𝐺 : 𝐵 –onto→ 𝐵 ∧ 0 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐺 ‘ 𝑦 ) = 0 )
12 7 10 11 syl2anc ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐺 ‘ 𝑦 ) = 0 )
13 oveq1 ⊢ ( 𝑎 = 𝑦 → ( 𝑎 + 𝑋 ) = ( 𝑦 + 𝑋 ) )
14 simpr ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
15 ovexd ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 + 𝑋 ) ∈ V )
16 4 13 14 15 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝑦 + 𝑋 ) )
17 16 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑦 ) = 0 ↔ ( 𝑦 + 𝑋 ) = 0 ) )
18 17 biimpd ⊢ ( ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑦 ) = 0 → ( 𝑦 + 𝑋 ) = 0 ) )
19 18 reximdva ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐵 ( 𝐺 ‘ 𝑦 ) = 0 → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) )
20 12 19 mpd ⊢ ( ( 𝜑 ∧ 𝐺 : 𝐵 –onto→ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 )
21 5 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐸 ∈ Mnd )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
23 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
24 1 3 21 22 23 mndcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 + 𝑋 ) ∈ 𝐵 )
25 24 4 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐵 )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) → 𝐺 : 𝐵 ⟶ 𝐵 )
27 fveq2 ⊢ ( 𝑥 = ( 𝑧 + 𝑦 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝑧 + 𝑦 ) ) )
28 27 eqeq2d ⊢ ( 𝑥 = ( 𝑧 + 𝑦 ) → ( 𝑧 = ( 𝐺 ‘ 𝑥 ) ↔ 𝑧 = ( 𝐺 ‘ ( 𝑧 + 𝑦 ) ) ) )
29 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐸 ∈ Mnd )
30 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
31 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
32 1 3 29 30 31 mndcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 + 𝑦 ) ∈ 𝐵 )
33 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
34 1 3 29 30 31 33 mndassd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑧 + 𝑦 ) + 𝑋 ) = ( 𝑧 + ( 𝑦 + 𝑋 ) ) )
35 oveq1 ⊢ ( 𝑎 = ( 𝑧 + 𝑦 ) → ( 𝑎 + 𝑋 ) = ( ( 𝑧 + 𝑦 ) + 𝑋 ) )
36 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑧 + 𝑦 ) + 𝑋 ) ∈ V )
37 4 35 32 36 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐺 ‘ ( 𝑧 + 𝑦 ) ) = ( ( 𝑧 + 𝑦 ) + 𝑋 ) )
38 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 + 𝑋 ) = 0 )
39 38 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 + ( 𝑦 + 𝑋 ) ) = ( 𝑧 + 0 ) )
40 1 3 2 mndrid ⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 + 0 ) = 𝑧 )
41 29 30 40 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 + 0 ) = 𝑧 )
42 39 41 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 = ( 𝑧 + ( 𝑦 + 𝑋 ) ) )
43 34 37 42 3eqtr4rd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 = ( 𝐺 ‘ ( 𝑧 + 𝑦 ) ) )
44 28 32 43 rspcedvdw ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 𝑧 = ( 𝐺 ‘ 𝑥 ) )
45 44 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 𝑧 = ( 𝐺 ‘ 𝑥 ) )
46 dffo3 ⊢ ( 𝐺 : 𝐵 –onto→ 𝐵 ↔ ( 𝐺 : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 𝑧 = ( 𝐺 ‘ 𝑥 ) ) )
47 26 45 46 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 + 𝑋 ) = 0 ) → 𝐺 : 𝐵 –onto→ 𝐵 )
48 47 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) → 𝐺 : 𝐵 –onto→ 𝐵 )
49 20 48 impbida ⊢ ( 𝜑 → ( 𝐺 : 𝐵 –onto→ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑋 ) = 0 ) )