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