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

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	crngcom	|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( Y .x. X ) )
6	1 2 3 4	opprmul	|- ( X .xb Y ) = ( Y .x. X )
7	5 6	eqtr4di	|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( X .xb Y ) )