Theorem crngoppr

Description: In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd ). (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	opprval.1	$$⊢B={\mathrm{Base}}_R$$
	opprval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	opprval.3	$$⊢O={opp}_r\left(R\right)$$
	opprmulfval.4	$$⊢\underset{\dot{}}{\bullet }={\cdot }_O$$
Assertion	crngoppr	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{\bullet }Y$$

Proof

Step	Hyp	Ref	Expression
1		opprval.1	$$⊢B={\mathrm{Base}}_R$$
2		opprval.2	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		opprval.3	$$⊢O={opp}_r\left(R\right)$$
4		opprmulfval.4	$$⊢\underset{\dot{}}{\bullet }={\cdot }_O$$
5	1 2	crngcom	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y=Y\underset{\dot{}}{·}X$$
6	1 2 3 4	opprmul	$$⊢X\underset{\dot{}}{\bullet }Y=Y\underset{\dot{}}{·}X$$
7	5 6	eqtr4di	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{\bullet }Y$$