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 = ( Base ` R )
	opprval.2	|- .x. = ( .r ` R )
	opprval.3	|- O = ( oppR ` R )
	opprmulfval.4	|- .xb = ( .r ` O )
Assertion	opprmul	|- ( X .xb Y ) = ( Y .x. X )

Proof

Step	Hyp	Ref	Expression
1		opprval.1	|- B = ( Base ` R )
2		opprval.2	|- .x. = ( .r ` R )
3		opprval.3	|- O = ( oppR ` R )
4		opprmulfval.4	|- .xb = ( .r ` O )
5	1 2 3 4	opprmulfval	|- .xb = tpos .x.
6	5	oveqi	|- ( X .xb Y ) = ( X tpos .x. Y )
7		ovtpos	|- ( X tpos .x. Y ) = ( Y .x. X )
8	6 7	eqtri	|- ( X .xb Y ) = ( Y .x. X )