Theorem opprmndb

Description: A class is a monoid if and only if its opposite (ring) is a monoid. (Contributed by SN, 20-Jun-2025)

	Ref	Expression
Hypothesis	opprgrp.o	|- O = ( oppR ` R )
Assertion	opprmndb	|- ( R e. Mnd <-> O e. Mnd )

Proof

Step	Hyp	Ref	Expression
1		opprgrp.o	|- O = ( oppR ` R )
2		baseid	|- Base = Slot ( Base ` ndx )
3		basendxnmulrndx	|- ( Base ` ndx ) =/= ( .r ` ndx )
4	1 2 3	opprlem	|- ( Base ` R ) = ( Base ` O )
5		plusgid	|- +g = Slot ( +g ` ndx )
6		plusgndxnmulrndx	|- ( +g ` ndx ) =/= ( .r ` ndx )
7	1 5 6	opprlem	|- ( +g ` R ) = ( +g ` O )
8	4 7	mndprop	|- ( R e. Mnd <-> O e. Mnd )