df-oppg

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	$⊢ {opp}_{𝑔} = (w \in V ⟼ w sSet ⟨+_{ndx}, tpos +_{w}⟩)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppg	$class {opp}_{𝑔}$
1		vw	$setvar w$
2		cvv	$class V$
3	1	cv	$setvar w$
4		csts	$class sSet$
5		cplusg	$class +_{𝑔}$
6		cnx	$class ndx$
7	6 5	cfv	$class +_{ndx}$
8	3 5	cfv	$class +_{w}$
9	8	ctpos	$class tpos +_{w}$
10	7 9	cop	$class ⟨+_{ndx}, tpos +_{w}⟩$
11	3 10 4	co	$class (w sSet ⟨+_{ndx}, tpos +_{w}⟩)$
12	1 2 11	cmpt	$class (w \in V ⟼ w sSet ⟨+_{ndx}, tpos +_{w}⟩)$
13	0 12	wceq	$wff {opp}_{𝑔} = (w \in V ⟼ w sSet ⟨+_{ndx}, tpos +_{w}⟩)$

Metamath Proof Explorer

Definition df-oppg

Detailed syntax breakdown