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