Metamath Proof Explorer

Theorem mndmolinv

Description: An element of a monoid that has a right inverse has at most one left inverse. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses mndmolinv.1 ⊢ 𝐵 = ( Base ‘ 𝑀 )
mndmolinv.2 ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
mndmolinv.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
mndmolinv.4 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( 𝐴 ( +g ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) )
Assertion mndmolinv ( 𝜑 → ∃* 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 mndmolinv.1 ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 mndmolinv.2 ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3 mndmolinv.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
4 mndmolinv.4 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( 𝐴 ( +g ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) )
5 nfv ⊢ Ⅎ 𝑦 ( 𝐴 ( +g ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 )
6 nfv ⊢ Ⅎ 𝑥 ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 )
7 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) )
8 7 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) ↔ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) )
9 5 6 8 cbvrexw ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐴 ( +g ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) )
10 9 biimpi ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐴 ( +g ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) )
11 4 10 syl ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) )
12 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → 𝑀 ∈ Mnd )
13 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → 𝑥 ∈ 𝐵 )
14 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
15 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
16 1 14 15 mndrid ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = 𝑥 )
17 12 13 16 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = 𝑥 )
18 17 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → 𝑥 = ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) )
19 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) )
20 19 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( 0g ‘ 𝑀 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) )
21 20 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ) )
22 18 21 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → 𝑥 = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ) )
23 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → 𝐴 ∈ 𝐵 )
24 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → 𝑦 ∈ 𝐵 )
25 13 23 24 3jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
26 1 14 mndass ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ) )
27 12 25 26 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ) )
28 27 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑦 ) )
29 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) )
30 29 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑦 ) )
31 1 14 15 mndlid ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑦 ) = 𝑦 )
32 12 24 31 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑦 ) = 𝑦 )
33 30 32 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑦 ) = 𝑦 )
34 22 28 33 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) ) → 𝑥 = 𝑦 )
35 34 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) → 𝑥 = 𝑦 ) )
36 35 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) → 𝑥 = 𝑦 ) )
37 36 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) → 𝑥 = 𝑦 ) ) )
38 37 reximdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐵 ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 0g ‘ 𝑀 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) → 𝑥 = 𝑦 ) ) )
39 11 38 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) → 𝑥 = 𝑦 ) )
40 nfv ⊢ Ⅎ 𝑦 ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 )
41 40 rmo2i ⊢ ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) → 𝑥 = 𝑦 ) → ∃* 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) )
42 39 41 syl ⊢ ( 𝜑 → ∃* 𝑥 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝑀 ) 𝐴 ) = ( 0g ‘ 𝑀 ) )