Theorem opprablb

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

	Ref	Expression
Hypothesis	opprgrp.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion	opprablb	⊢ ( 𝑅 ∈ Abel ↔ 𝑂 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		opprgrp.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2		baseid	⊢ Base = Slot ( Base ‘ ndx )
3		basendxnmulrndx	⊢ ( Base ‘ ndx ) ≠ ( .r ‘ ndx )
4	1 2 3	opprlem	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
5		plusgid	⊢ +g = Slot ( +g ‘ ndx )
6		plusgndxnmulrndx	⊢ ( +g ‘ ndx ) ≠ ( .r ‘ ndx )
7	1 5 6	opprlem	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
8	4 7	ablprop	⊢ ( 𝑅 ∈ Abel ↔ 𝑂 ∈ Abel )