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 )