Metamath Proof Explorer


Theorem mndinvmod

Description: Uniqueness of an inverse element in a monoid, if it exists. (Contributed by AV, 20-Jan-2024)

Ref Expression
Hypotheses mndinvmod.b 𝐵 = ( Base ‘ 𝐺 )
mndinvmod.0 0 = ( 0g𝐺 )
mndinvmod.p + = ( +g𝐺 )
mndinvmod.m ( 𝜑𝐺 ∈ Mnd )
mndinvmod.a ( 𝜑𝐴𝐵 )
Assertion mndinvmod ( 𝜑 → ∃* 𝑤𝐵 ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 mndinvmod.b 𝐵 = ( Base ‘ 𝐺 )
2 mndinvmod.0 0 = ( 0g𝐺 )
3 mndinvmod.p + = ( +g𝐺 )
4 mndinvmod.m ( 𝜑𝐺 ∈ Mnd )
5 mndinvmod.a ( 𝜑𝐴𝐵 )
6 simpl ( ( 𝑤𝐵𝑣𝐵 ) → 𝑤𝐵 )
7 1 3 2 mndrid ( ( 𝐺 ∈ Mnd ∧ 𝑤𝐵 ) → ( 𝑤 + 0 ) = 𝑤 )
8 4 6 7 syl2an ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) → ( 𝑤 + 0 ) = 𝑤 )
9 8 eqcomd ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) → 𝑤 = ( 𝑤 + 0 ) )
10 9 adantr ( ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) ∧ ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) ) → 𝑤 = ( 𝑤 + 0 ) )
11 oveq2 ( 0 = ( 𝐴 + 𝑣 ) → ( 𝑤 + 0 ) = ( 𝑤 + ( 𝐴 + 𝑣 ) ) )
12 11 eqcoms ( ( 𝐴 + 𝑣 ) = 0 → ( 𝑤 + 0 ) = ( 𝑤 + ( 𝐴 + 𝑣 ) ) )
13 12 adantl ( ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) → ( 𝑤 + 0 ) = ( 𝑤 + ( 𝐴 + 𝑣 ) ) )
14 13 adantl ( ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) → ( 𝑤 + 0 ) = ( 𝑤 + ( 𝐴 + 𝑣 ) ) )
15 14 adantl ( ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) ∧ ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) ) → ( 𝑤 + 0 ) = ( 𝑤 + ( 𝐴 + 𝑣 ) ) )
16 4 adantr ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) → 𝐺 ∈ Mnd )
17 6 adantl ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) → 𝑤𝐵 )
18 5 adantr ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) → 𝐴𝐵 )
19 simpr ( ( 𝑤𝐵𝑣𝐵 ) → 𝑣𝐵 )
20 19 adantl ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) → 𝑣𝐵 )
21 1 3 mndass ( ( 𝐺 ∈ Mnd ∧ ( 𝑤𝐵𝐴𝐵𝑣𝐵 ) ) → ( ( 𝑤 + 𝐴 ) + 𝑣 ) = ( 𝑤 + ( 𝐴 + 𝑣 ) ) )
22 21 eqcomd ( ( 𝐺 ∈ Mnd ∧ ( 𝑤𝐵𝐴𝐵𝑣𝐵 ) ) → ( 𝑤 + ( 𝐴 + 𝑣 ) ) = ( ( 𝑤 + 𝐴 ) + 𝑣 ) )
23 16 17 18 20 22 syl13anc ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) → ( 𝑤 + ( 𝐴 + 𝑣 ) ) = ( ( 𝑤 + 𝐴 ) + 𝑣 ) )
24 23 adantr ( ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) ∧ ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) ) → ( 𝑤 + ( 𝐴 + 𝑣 ) ) = ( ( 𝑤 + 𝐴 ) + 𝑣 ) )
25 oveq1 ( ( 𝑤 + 𝐴 ) = 0 → ( ( 𝑤 + 𝐴 ) + 𝑣 ) = ( 0 + 𝑣 ) )
26 25 adantr ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) → ( ( 𝑤 + 𝐴 ) + 𝑣 ) = ( 0 + 𝑣 ) )
27 26 adantr ( ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) → ( ( 𝑤 + 𝐴 ) + 𝑣 ) = ( 0 + 𝑣 ) )
28 27 adantl ( ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) ∧ ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) ) → ( ( 𝑤 + 𝐴 ) + 𝑣 ) = ( 0 + 𝑣 ) )
29 1 3 2 mndlid ( ( 𝐺 ∈ Mnd ∧ 𝑣𝐵 ) → ( 0 + 𝑣 ) = 𝑣 )
30 4 19 29 syl2an ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) → ( 0 + 𝑣 ) = 𝑣 )
31 30 adantr ( ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) ∧ ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) ) → ( 0 + 𝑣 ) = 𝑣 )
32 24 28 31 3eqtrd ( ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) ∧ ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) ) → ( 𝑤 + ( 𝐴 + 𝑣 ) ) = 𝑣 )
33 10 15 32 3eqtrd ( ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) ∧ ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) ) → 𝑤 = 𝑣 )
34 33 ex ( ( 𝜑 ∧ ( 𝑤𝐵𝑣𝐵 ) ) → ( ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) → 𝑤 = 𝑣 ) )
35 34 ralrimivva ( 𝜑 → ∀ 𝑤𝐵𝑣𝐵 ( ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) → 𝑤 = 𝑣 ) )
36 oveq1 ( 𝑤 = 𝑣 → ( 𝑤 + 𝐴 ) = ( 𝑣 + 𝐴 ) )
37 36 eqeq1d ( 𝑤 = 𝑣 → ( ( 𝑤 + 𝐴 ) = 0 ↔ ( 𝑣 + 𝐴 ) = 0 ) )
38 oveq2 ( 𝑤 = 𝑣 → ( 𝐴 + 𝑤 ) = ( 𝐴 + 𝑣 ) )
39 38 eqeq1d ( 𝑤 = 𝑣 → ( ( 𝐴 + 𝑤 ) = 0 ↔ ( 𝐴 + 𝑣 ) = 0 ) )
40 37 39 anbi12d ( 𝑤 = 𝑣 → ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ↔ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) )
41 40 rmo4 ( ∃* 𝑤𝐵 ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ↔ ∀ 𝑤𝐵𝑣𝐵 ( ( ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ∧ ( ( 𝑣 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑣 ) = 0 ) ) → 𝑤 = 𝑣 ) )
42 35 41 sylibr ( 𝜑 → ∃* 𝑤𝐵 ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) )