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. = ( 0g ` G )
mndinvmod.p
|- .+ = ( +g ` G )
mndinvmod.m
|- ( ph -> G e. Mnd )
mndinvmod.a
|- ( ph -> A e. B )
Assertion mndinvmod
|- ( ph -> E* w e. B ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) )

Proof

Step Hyp Ref Expression
1 mndinvmod.b
 |-  B = ( Base ` G )
2 mndinvmod.0
 |-  .0. = ( 0g ` G )
3 mndinvmod.p
 |-  .+ = ( +g ` G )
4 mndinvmod.m
 |-  ( ph -> G e. Mnd )
5 mndinvmod.a
 |-  ( ph -> A e. B )
6 simpl
 |-  ( ( w e. B /\ v e. B ) -> w e. B )
7 1 3 2 mndrid
 |-  ( ( G e. Mnd /\ w e. B ) -> ( w .+ .0. ) = w )
8 4 6 7 syl2an
 |-  ( ( ph /\ ( w e. B /\ v e. B ) ) -> ( w .+ .0. ) = w )
9 8 eqcomd
 |-  ( ( ph /\ ( w e. B /\ v e. B ) ) -> w = ( w .+ .0. ) )
10 9 adantr
 |-  ( ( ( ph /\ ( w e. B /\ v e. 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
 |-  ( ( ( ph /\ ( w e. B /\ v e. B ) ) /\ ( ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) /\ ( ( v .+ A ) = .0. /\ ( A .+ v ) = .0. ) ) ) -> ( w .+ .0. ) = ( w .+ ( A .+ v ) ) )
16 4 adantr
 |-  ( ( ph /\ ( w e. B /\ v e. B ) ) -> G e. Mnd )
17 6 adantl
 |-  ( ( ph /\ ( w e. B /\ v e. B ) ) -> w e. B )
18 5 adantr
 |-  ( ( ph /\ ( w e. B /\ v e. B ) ) -> A e. B )
19 simpr
 |-  ( ( w e. B /\ v e. B ) -> v e. B )
20 19 adantl
 |-  ( ( ph /\ ( w e. B /\ v e. B ) ) -> v e. B )
21 1 3 mndass
 |-  ( ( G e. Mnd /\ ( w e. B /\ A e. B /\ v e. B ) ) -> ( ( w .+ A ) .+ v ) = ( w .+ ( A .+ v ) ) )
22 21 eqcomd
 |-  ( ( G e. Mnd /\ ( w e. B /\ A e. B /\ v e. B ) ) -> ( w .+ ( A .+ v ) ) = ( ( w .+ A ) .+ v ) )
23 16 17 18 20 22 syl13anc
 |-  ( ( ph /\ ( w e. B /\ v e. B ) ) -> ( w .+ ( A .+ v ) ) = ( ( w .+ A ) .+ v ) )
24 23 adantr
 |-  ( ( ( ph /\ ( w e. B /\ v e. 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
 |-  ( ( ( ph /\ ( w e. B /\ v e. B ) ) /\ ( ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) /\ ( ( v .+ A ) = .0. /\ ( A .+ v ) = .0. ) ) ) -> ( ( w .+ A ) .+ v ) = ( .0. .+ v ) )
29 1 3 2 mndlid
 |-  ( ( G e. Mnd /\ v e. B ) -> ( .0. .+ v ) = v )
30 4 19 29 syl2an
 |-  ( ( ph /\ ( w e. B /\ v e. B ) ) -> ( .0. .+ v ) = v )
31 30 adantr
 |-  ( ( ( ph /\ ( w e. B /\ v e. B ) ) /\ ( ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) /\ ( ( v .+ A ) = .0. /\ ( A .+ v ) = .0. ) ) ) -> ( .0. .+ v ) = v )
32 24 28 31 3eqtrd
 |-  ( ( ( ph /\ ( w e. B /\ v e. B ) ) /\ ( ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) /\ ( ( v .+ A ) = .0. /\ ( A .+ v ) = .0. ) ) ) -> ( w .+ ( A .+ v ) ) = v )
33 10 15 32 3eqtrd
 |-  ( ( ( ph /\ ( w e. B /\ v e. B ) ) /\ ( ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) /\ ( ( v .+ A ) = .0. /\ ( A .+ v ) = .0. ) ) ) -> w = v )
34 33 ex
 |-  ( ( ph /\ ( w e. B /\ v e. B ) ) -> ( ( ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) /\ ( ( v .+ A ) = .0. /\ ( A .+ v ) = .0. ) ) -> w = v ) )
35 34 ralrimivva
 |-  ( ph -> A. w e. B A. v e. 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
 |-  ( E* w e. B ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) <-> A. w e. B A. v e. B ( ( ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) /\ ( ( v .+ A ) = .0. /\ ( A .+ v ) = .0. ) ) -> w = v ) )
42 35 41 sylibr
 |-  ( ph -> E* w e. B ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) )