Metamath Proof Explorer

Definition df-ginv

Description: Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-ginv	$⊢ inv = (g \in GrpOp ⟼ (x \in ran g ⟼ (ι z \in ran g \| z g x = GId (g))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgn	$class inv$
1		vg	$setvar g$
2		cgr	$class GrpOp$
3		vx	$setvar x$
4	1	cv	$setvar g$
5	4	crn	$class ran g$
6		vz	$setvar z$
7	6	cv	$setvar z$
8	3	cv	$setvar x$
9	7 8 4	co	$class (z g x)$
10		cgi	$class GId$
11	4 10	cfv	$class GId (g)$
12	9 11	wceq	$wff z g x = GId (g)$
13	12 6 5	crio	$class (ι z \in ran g \| z g x = GId (g))$
14	3 5 13	cmpt	$class (x \in ran g ⟼ (ι z \in ran g \| z g x = GId (g)))$
15	1 2 14	cmpt	$class (g \in GrpOp ⟼ (x \in ran g ⟼ (ι z \in ran g \| z g x = GId (g))))$
16	0 15	wceq	$wff inv = (g \in GrpOp ⟼ (x \in ran g ⟼ (ι z \in ran g \| z g x = GId (g))))$