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

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 ) )