Theorem opprmul

Description: Value of the multiplication operation of an opposite ring. Hypotheses eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Aug-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	opprmul	$$⊢X\underset{\dot{}}{\bullet }Y=Y\underset{\dot{}}{·}X$$

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 3 4	opprmulfval	$$⊢\underset{\dot{}}{\bullet }=tpos\underset{\dot{}}{·}$$
6	5	oveqi	$$⊢X\underset{\dot{}}{\bullet }Y=Xtpos\underset{\dot{}}{·}Y$$
7		ovtpos	$$⊢Xtpos\underset{\dot{}}{·}Y=Y\underset{\dot{}}{·}X$$
8	6 7	eqtri	$$⊢X\underset{\dot{}}{\bullet }Y=Y\underset{\dot{}}{·}X$$