This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )