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

Metamath Proof Explorer

Theorem rinvmod

Description: Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovmo . (Contributed by AV, 31-Dec-2023)

Ref Expression
Hypotheses rinvmod.b 
|- B = ( Base ` G )
rinvmod.0 
|- .0. = ( 0g ` G )
rinvmod.p 
|- .+ = ( +g ` G )
rinvmod.m 
|- ( ph -> G e. CMnd )
rinvmod.a 
|- ( ph -> A e. B )
Assertion rinvmod 
|- ( ph -> E* w e. B ( A .+ w ) = .0. )

Proof

Step Hyp Ref Expression
1 rinvmod.b 
 |-  B = ( Base ` G )
2 rinvmod.0 
 |-  .0. = ( 0g ` G )
3 rinvmod.p 
 |-  .+ = ( +g ` G )
4 rinvmod.m 
 |-  ( ph -> G e. CMnd )
5 rinvmod.a 
 |-  ( ph -> A e. B )
6 4 adantr 
 |-  ( ( ph /\ w e. B ) -> G e. CMnd )
7 simpr 
 |-  ( ( ph /\ w e. B ) -> w e. B )
8 5 adantr 
 |-  ( ( ph /\ w e. B ) -> A e. B )
9 1 3 cmncom 
 |-  ( ( G e. CMnd /\ w e. B /\ A e. B ) -> ( w .+ A ) = ( A .+ w ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ph /\ w e. B ) -> ( w .+ A ) = ( A .+ w ) )
11 10 adantr 
 |-  ( ( ( ph /\ w e. B ) /\ ( A .+ w ) = .0. ) -> ( w .+ A ) = ( A .+ w ) )
12 simpr 
 |-  ( ( ( ph /\ w e. B ) /\ ( A .+ w ) = .0. ) -> ( A .+ w ) = .0. )
13 11 12 eqtrd 
 |-  ( ( ( ph /\ w e. B ) /\ ( A .+ w ) = .0. ) -> ( w .+ A ) = .0. )
14 13 12 jca 
 |-  ( ( ( ph /\ w e. B ) /\ ( A .+ w ) = .0. ) -> ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) )
15 14 ex 
 |-  ( ( ph /\ w e. B ) -> ( ( A .+ w ) = .0. -> ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) ) )
16 15 ralrimiva 
 |-  ( ph -> A. w e. B ( ( A .+ w ) = .0. -> ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) ) )
17 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
18 4 17 syl 
 |-  ( ph -> G e. Mnd )
19 1 2 3 18 5 mndinvmod 
 |-  ( ph -> E* w e. B ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) )
20 rmoim 
 |-  ( A. w e. B ( ( A .+ w ) = .0. -> ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) ) -> ( E* w e. B ( ( w .+ A ) = .0. /\ ( A .+ w ) = .0. ) -> E* w e. B ( A .+ w ) = .0. ) )
21 16 19 20 sylc 
 |-  ( ph -> E* w e. B ( A .+ w ) = .0. )