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 𝐵 = ( Base ‘ 𝐺 )
rinvmod.0 0 = ( 0g𝐺 )
rinvmod.p + = ( +g𝐺 )
rinvmod.m ( 𝜑𝐺 ∈ CMnd )
rinvmod.a ( 𝜑𝐴𝐵 )
Assertion rinvmod ( 𝜑 → ∃* 𝑤𝐵 ( 𝐴 + 𝑤 ) = 0 )

Proof

Step Hyp Ref Expression
1 rinvmod.b 𝐵 = ( Base ‘ 𝐺 )
2 rinvmod.0 0 = ( 0g𝐺 )
3 rinvmod.p + = ( +g𝐺 )
4 rinvmod.m ( 𝜑𝐺 ∈ CMnd )
5 rinvmod.a ( 𝜑𝐴𝐵 )
6 4 adantr ( ( 𝜑𝑤𝐵 ) → 𝐺 ∈ CMnd )
7 simpr ( ( 𝜑𝑤𝐵 ) → 𝑤𝐵 )
8 5 adantr ( ( 𝜑𝑤𝐵 ) → 𝐴𝐵 )
9 1 3 cmncom ( ( 𝐺 ∈ CMnd ∧ 𝑤𝐵𝐴𝐵 ) → ( 𝑤 + 𝐴 ) = ( 𝐴 + 𝑤 ) )
10 6 7 8 9 syl3anc ( ( 𝜑𝑤𝐵 ) → ( 𝑤 + 𝐴 ) = ( 𝐴 + 𝑤 ) )
11 10 adantr ( ( ( 𝜑𝑤𝐵 ) ∧ ( 𝐴 + 𝑤 ) = 0 ) → ( 𝑤 + 𝐴 ) = ( 𝐴 + 𝑤 ) )
12 simpr ( ( ( 𝜑𝑤𝐵 ) ∧ ( 𝐴 + 𝑤 ) = 0 ) → ( 𝐴 + 𝑤 ) = 0 )
13 11 12 eqtrd ( ( ( 𝜑𝑤𝐵 ) ∧ ( 𝐴 + 𝑤 ) = 0 ) → ( 𝑤 + 𝐴 ) = 0 )
14 13 12 jca ( ( ( 𝜑𝑤𝐵 ) ∧ ( 𝐴 + 𝑤 ) = 0 ) → ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) )
15 14 ex ( ( 𝜑𝑤𝐵 ) → ( ( 𝐴 + 𝑤 ) = 0 → ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ) )
16 15 ralrimiva ( 𝜑 → ∀ 𝑤𝐵 ( ( 𝐴 + 𝑤 ) = 0 → ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ) )
17 cmnmnd ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
18 4 17 syl ( 𝜑𝐺 ∈ Mnd )
19 1 2 3 18 5 mndinvmod ( 𝜑 → ∃* 𝑤𝐵 ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) )
20 rmoim ( ∀ 𝑤𝐵 ( ( 𝐴 + 𝑤 ) = 0 → ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) ) → ( ∃* 𝑤𝐵 ( ( 𝑤 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑤 ) = 0 ) → ∃* 𝑤𝐵 ( 𝐴 + 𝑤 ) = 0 ) )
21 16 19 20 sylc ( 𝜑 → ∃* 𝑤𝐵 ( 𝐴 + 𝑤 ) = 0 )