MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-oppg Structured version   Visualization version   GIF version

Definition df-oppg 19251
Description: Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 20225 does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015.)
Assertion
Ref Expression
df-oppg oppg = (𝑀 ∈ V ↦ (𝑀 sSet ⟨(+gβ€˜ndx), tpos (+gβ€˜π‘€)⟩))

Detailed syntax breakdown of Definition df-oppg
StepHypRef Expression
1 coppg 19250 . 2 class oppg
2 vw . . 3 setvar 𝑀
3 cvv 3472 . . 3 class V
42cv 1538 . . . 4 class 𝑀
5 cnx 17130 . . . . . 6 class ndx
6 cplusg 17201 . . . . . 6 class +g
75, 6cfv 6542 . . . . 5 class (+gβ€˜ndx)
84, 6cfv 6542 . . . . . 6 class (+gβ€˜π‘€)
98ctpos 8212 . . . . 5 class tpos (+gβ€˜π‘€)
107, 9cop 4633 . . . 4 class ⟨(+gβ€˜ndx), tpos (+gβ€˜π‘€)⟩
11 csts 17100 . . . 4 class sSet
124, 10, 11co 7411 . . 3 class (𝑀 sSet ⟨(+gβ€˜ndx), tpos (+gβ€˜π‘€)⟩)
132, 3, 12cmpt 5230 . 2 class (𝑀 ∈ V ↦ (𝑀 sSet ⟨(+gβ€˜ndx), tpos (+gβ€˜π‘€)⟩))
141, 13wceq 1539 1 wff oppg = (𝑀 ∈ V ↦ (𝑀 sSet ⟨(+gβ€˜ndx), tpos (+gβ€˜π‘€)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  oppgval  19252
  Copyright terms: Public domain W3C validator