Metamath Proof Explorer

Theorem mndlactfo

Description: An element X of a monoid E is left-invertible iff its left-translation F is surjective. See also grplactf1o . (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 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion mndlactfo ( 𝜑 → ( 𝐹 : 𝐵 –onto→ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑋 + 𝑦 ) = 0 ) )

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 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 oveq2 ⊢ ( 𝑎 = 𝑦 → ( 𝑋 + 𝑎 ) = ( 𝑋 + 𝑦 ) )
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 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
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 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
31 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
32 1 3 29 30 31 mndcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 + 𝑧 ) ∈ 𝐵 )
33 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
34 1 3 29 33 30 31 mndassd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑋 + 𝑦 ) + 𝑧 ) = ( 𝑋 + ( 𝑦 + 𝑧 ) ) )
35 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑋 + 𝑦 ) = 0 )
36 35 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑋 + 𝑦 ) + 𝑧 ) = ( 0 + 𝑧 ) )
37 1 3 2 mndlid ⊢ ( ( 𝐸 ∈ Mnd ∧ 𝑧 ∈ 𝐵 ) → ( 0 + 𝑧 ) = 𝑧 )
38 29 31 37 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 0 + 𝑧 ) = 𝑧 )
39 36 38 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 = ( ( 𝑋 + 𝑦 ) + 𝑧 ) )
40 oveq2 ⊢ ( 𝑎 = ( 𝑦 + 𝑧 ) → ( 𝑋 + 𝑎 ) = ( 𝑋 + ( 𝑦 + 𝑧 ) ) )
41 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑋 + ( 𝑦 + 𝑧 ) ) ∈ V )
42 4 40 32 41 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 0 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) = ( 𝑋 + ( 𝑦 + 𝑧 ) ) )
43 34 39 42 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑦 ) = 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 ) )