Theorem opprgrpb

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

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

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	grpprop	|- ( R e. Grp <-> O e. Grp )