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

Metamath Proof Explorer

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 ⊢ opp r = f ∈ V ⟼ f sSet ⋅ ndx tpos ⋅ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 coppr class opp r
1 vf setvar f
2 cvv class V
3 1 cv setvar f
4 csts class sSet
5 cmulr class ⋅ 𝑟
6 cnx class ndx
7 6 5 cfv class ⋅ ndx
8 3 5 cfv class ⋅ f
9 8 ctpos class tpos ⋅ f
10 7 9 cop class ⋅ ndx tpos ⋅ f
11 3 10 4 co class f sSet ⋅ ndx tpos ⋅ f
12 1 2 11 cmpt class f ∈ V ⟼ f sSet ⋅ ndx tpos ⋅ f
13 0 12 wceq wff opp r = f ∈ V ⟼ f sSet ⋅ ndx tpos ⋅ f