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

Metamath Proof Explorer

Theorem mndlrinvb

Description: In a monoid, if an element has both a left-inverse and a right-inverse, they are equal. (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses mndlrinv.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
mndlrinv.z ⊢ 0 = ( 0g ‘ 𝐸 )
mndlrinv.p ⊢ + = ( +g ‘ 𝐸 )
mndlrinv.e ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
mndlrinv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion mndlrinvb ( 𝜑 → ( ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ) ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 mndlrinv.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
2 mndlrinv.z ⊢ 0 = ( 0g ‘ 𝐸 )
3 mndlrinv.p ⊢ + = ( +g ‘ 𝐸 )
4 mndlrinv.e ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
5 mndlrinv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 oveq2 ⊢ ( 𝑧 = 𝑢 → ( 𝑋 + 𝑧 ) = ( 𝑋 + 𝑢 ) )
7 6 eqeq1d ⊢ ( 𝑧 = 𝑢 → ( ( 𝑋 + 𝑧 ) = 0 ↔ ( 𝑋 + 𝑢 ) = 0 ) )
8 oveq1 ⊢ ( 𝑧 = 𝑢 → ( 𝑧 + 𝑋 ) = ( 𝑢 + 𝑋 ) )
9 8 eqeq1d ⊢ ( 𝑧 = 𝑢 → ( ( 𝑧 + 𝑋 ) = 0 ↔ ( 𝑢 + 𝑋 ) = 0 ) )
10 7 9 anbi12d ⊢ ( 𝑧 = 𝑢 → ( ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ↔ ( ( 𝑋 + 𝑢 ) = 0 ∧ ( 𝑢 + 𝑋 ) = 0 ) ) )
11 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝑢 ∈ 𝐵 )
12 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( 𝑋 + 𝑢 ) = 0 )
13 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝐸 ∈ Mnd )
14 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝑋 ∈ 𝐵 )
15 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝑣 ∈ 𝐵 )
16 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( 𝑣 + 𝑋 ) = 0 )
17 1 2 3 13 14 15 11 16 12 mndlrinv ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → 𝑣 = 𝑢 )
18 17 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( 𝑣 + 𝑋 ) = ( 𝑢 + 𝑋 ) )
19 18 16 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( 𝑢 + 𝑋 ) = 0 )
20 12 19 jca ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ( ( 𝑋 + 𝑢 ) = 0 ∧ ( 𝑢 + 𝑋 ) = 0 ) )
21 10 11 20 rspcedvdw ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑋 + 𝑢 ) = 0 ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) )
22 21 r19.29an ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 + 𝑋 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) )
23 22 an42ds ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ) ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑣 + 𝑋 ) = 0 ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) )
24 23 r19.29an ⊢ ( ( ( 𝜑 ∧ ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ) ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) )
25 24 anasss ⊢ ( ( 𝜑 ∧ ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ) ) → ∃ 𝑧 ∈ 𝐵 ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) )
26 oveq2 ⊢ ( 𝑢 = 𝑧 → ( 𝑋 + 𝑢 ) = ( 𝑋 + 𝑧 ) )
27 26 eqeq1d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑋 + 𝑢 ) = 0 ↔ ( 𝑋 + 𝑧 ) = 0 ) )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ) → 𝑧 ∈ 𝐵 )
29 simprl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ) → ( 𝑋 + 𝑧 ) = 0 )
30 27 28 29 rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ) → ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 )
31 oveq1 ⊢ ( 𝑣 = 𝑧 → ( 𝑣 + 𝑋 ) = ( 𝑧 + 𝑋 ) )
32 31 eqeq1d ⊢ ( 𝑣 = 𝑧 → ( ( 𝑣 + 𝑋 ) = 0 ↔ ( 𝑧 + 𝑋 ) = 0 ) )
33 simprr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ) → ( 𝑧 + 𝑋 ) = 0 )
34 32 28 33 rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ) → ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 )
35 30 34 jca ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ) → ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ) )
36 35 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ 𝐵 ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ) → ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ) )
37 25 36 impbida ⊢ ( 𝜑 → ( ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ) ↔ ∃ 𝑧 ∈ 𝐵 ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ) )
38 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑋 + 𝑦 ) = ( 𝑋 + 𝑧 ) )
39 38 eqeq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑋 + 𝑦 ) = 0 ↔ ( 𝑋 + 𝑧 ) = 0 ) )
40 oveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 + 𝑋 ) = ( 𝑧 + 𝑋 ) )
41 40 eqeq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 + 𝑋 ) = 0 ↔ ( 𝑧 + 𝑋 ) = 0 ) )
42 39 41 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ↔ ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) ) )
43 42 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ↔ ∃ 𝑧 ∈ 𝐵 ( ( 𝑋 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑋 ) = 0 ) )
44 37 43 bitr4di ⊢ ( 𝜑 → ( ( ∃ 𝑢 ∈ 𝐵 ( 𝑋 + 𝑢 ) = 0 ∧ ∃ 𝑣 ∈ 𝐵 ( 𝑣 + 𝑋 ) = 0 ) ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 + 𝑦 ) = 0 ∧ ( 𝑦 + 𝑋 ) = 0 ) ) )