Definition df-oppr 20481

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.)

Assertion

Ref	Expression
df-oppr	⊢ oppr = (𝑓 ∈ V ↦ (𝑓 sSet ⟨(.r‘ndx), tpos (.r‘𝑓)⟩))

Detailed syntax breakdown of Definition df-oppr

Step	Hyp	Ref	Expression
1		coppr 20480	. 2 class oppr
2		vf	. . 3 setvar 𝑓
3		cvv 3450	. . 3 class V
4	2	cv 1569	. . . 4 class 𝑓
5		cnx 17288	. . . . . 6 class ndx
6		cmulr 17346	. . . . . 6 class .r
7	5, 6	cfv 6533	. . . . 5 class (.r‘ndx)
8	4, 6	cfv 6533	. . . . . 6 class (.r‘𝑓)
9	8	ctpos 8224	. . . . 5 class tpos (.r‘𝑓)
10	7, 9	cop 4590	. . . 4 class ⟨(.r‘ndx), tpos (.r‘𝑓)⟩
11		csts 17258	. . . 4 class sSet
12	4, 10, 11	co 7414	. . 3 class (𝑓 sSet ⟨(.r‘ndx), tpos (.r‘𝑓)⟩)
13	2, 3, 12	cmpt 5186	. 2 class (𝑓 ∈ V ↦ (𝑓 sSet ⟨(.r‘ndx), tpos (.r‘𝑓)⟩))
14	1, 13	wceq 1570	1 wff oppr = (𝑓 ∈ V ↦ (𝑓 sSet ⟨(.r‘ndx), tpos (.r‘𝑓)⟩))

This definition is used by:  opprval  20482