Description: Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-oppg | |- oppG = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , tpos ( +g ` w ) >. ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | coppg | |- oppG |
|
| 1 | vw | |- w |
|
| 2 | cvv | |- _V |
|
| 3 | 1 | cv | |- w |
| 4 | csts | |- sSet |
|
| 5 | cplusg | |- +g |
|
| 6 | cnx | |- ndx |
|
| 7 | 6 5 | cfv | |- ( +g ` ndx ) |
| 8 | 3 5 | cfv | |- ( +g ` w ) |
| 9 | 8 | ctpos | |- tpos ( +g ` w ) |
| 10 | 7 9 | cop | |- <. ( +g ` ndx ) , tpos ( +g ` w ) >. |
| 11 | 3 10 4 | co | |- ( w sSet <. ( +g ` ndx ) , tpos ( +g ` w ) >. ) |
| 12 | 1 2 11 | cmpt | |- ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , tpos ( +g ` w ) >. ) ) |
| 13 | 0 12 | wceq | |- oppG = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , tpos ( +g ` w ) >. ) ) |