Definition df-oppr

Description: Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Assertion	df-oppr	|- oppR = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppr	|- oppR
1		vf	|- f
2		cvv	|- _V
3	1	cv	|- f
4		csts	|- sSet
5		cmulr	|- .r
6		cnx	|- ndx
7	6 5	cfv	|- ( .r ` ndx )
8	3 5	cfv	|- ( .r ` f )
9	8	ctpos	|- tpos ( .r ` f )
10	7 9	cop	|- <. ( .r ` ndx ) , tpos ( .r ` f ) >.
11	3 10 4	co	|- ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. )
12	1 2 11	cmpt	|- ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
13	0 12	wceq	|- oppR = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )