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={opp}_r\left(R\right)$$
Assertion	opprgrpb	$$⊢R\in \mathrm{Grp}\leftrightarrow O\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		opprgrp.o	$$⊢O={opp}_r\left(R\right)$$
2		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
3		basendxnmulrndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
4	1 2 3	opprlem	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
5		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
6		plusgndxnmulrndx	$$⊢{+}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
7	1 5 6	opprlem	$$⊢{+}_R={+}_O$$
8	4 7	grpprop	$$⊢R\in \mathrm{Grp}\leftrightarrow O\in \mathrm{Grp}$$