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 B = Base G
mndinvmod.0 0 ˙ = 0 G
mndinvmod.p + ˙ = + G
mndinvmod.m φ G Mnd
mndinvmod.a φ A B
Assertion mndinvmod φ * w B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙

Proof

Step Hyp Ref Expression
1 mndinvmod.b B = Base G
2 mndinvmod.0 0 ˙ = 0 G
3 mndinvmod.p + ˙ = + G
4 mndinvmod.m φ G Mnd
5 mndinvmod.a φ A B
6 simpl w B v B w B
7 1 3 2 mndrid G Mnd w B w + ˙ 0 ˙ = w
8 4 6 7 syl2an φ w B v B w + ˙ 0 ˙ = w
9 8 eqcomd φ w B v B w = w + ˙ 0 ˙
10 9 adantr φ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w = w + ˙ 0 ˙
11 oveq2 0 ˙ = A + ˙ v w + ˙ 0 ˙ = w + ˙ A + ˙ v
12 11 eqcoms A + ˙ v = 0 ˙ w + ˙ 0 ˙ = w + ˙ A + ˙ v
13 12 adantl v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w + ˙ 0 ˙ = w + ˙ A + ˙ v
14 13 adantl w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w + ˙ 0 ˙ = w + ˙ A + ˙ v
15 14 adantl φ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w + ˙ 0 ˙ = w + ˙ A + ˙ v
16 4 adantr φ w B v B G Mnd
17 6 adantl φ w B v B w B
18 5 adantr φ w B v B A B
19 simpr w B v B v B
20 19 adantl φ w B v B v B
21 1 3 mndass G Mnd w B A B v B w + ˙ A + ˙ v = w + ˙ A + ˙ v
22 21 eqcomd G Mnd w B A B v B w + ˙ A + ˙ v = w + ˙ A + ˙ v
23 16 17 18 20 22 syl13anc φ w B v B w + ˙ A + ˙ v = w + ˙ A + ˙ v
24 23 adantr φ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w + ˙ A + ˙ v = w + ˙ A + ˙ v
25 oveq1 w + ˙ A = 0 ˙ w + ˙ A + ˙ v = 0 ˙ + ˙ v
26 25 adantr w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ w + ˙ A + ˙ v = 0 ˙ + ˙ v
27 26 adantr w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w + ˙ A + ˙ v = 0 ˙ + ˙ v
28 27 adantl φ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w + ˙ A + ˙ v = 0 ˙ + ˙ v
29 1 3 2 mndlid G Mnd v B 0 ˙ + ˙ v = v
30 4 19 29 syl2an φ w B v B 0 ˙ + ˙ v = v
31 30 adantr φ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ 0 ˙ + ˙ v = v
32 24 28 31 3eqtrd φ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w + ˙ A + ˙ v = v
33 10 15 32 3eqtrd φ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w = v
34 33 ex φ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w = v
35 34 ralrimivva φ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w = v
36 oveq1 w = v w + ˙ A = v + ˙ A
37 36 eqeq1d w = v w + ˙ A = 0 ˙ v + ˙ A = 0 ˙
38 oveq2 w = v A + ˙ w = A + ˙ v
39 38 eqeq1d w = v A + ˙ w = 0 ˙ A + ˙ v = 0 ˙
40 37 39 anbi12d w = v w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙
41 40 rmo4 * w B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ w B v B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙ v + ˙ A = 0 ˙ A + ˙ v = 0 ˙ w = v
42 35 41 sylibr φ * w B w + ˙ A = 0 ˙ A + ˙ w = 0 ˙