MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ginv Unicode version

Definition df-ginv 20860
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.)
Assertion
Ref Expression
df-ginv  |-  inv  =  ( g  e.  GrpOp  |->  ( x  e.  ran  g  |->  ( iota_ z  e. 
ran  g ( z g x )  =  (GId `  g )
) ) )
Distinct variable group:    x, g, z

Detailed syntax breakdown of Definition df-ginv
StepHypRef Expression
1 cgn 20855 . 2  class  inv
2 vg . . 3  set  g
3 cgr 20853 . . 3  class  GrpOp
4 vx . . . 4  set  x
52cv 1622 . . . . 5  class  g
65crn 4690 . . . 4  class  ran  g
7 vz . . . . . . . 8  set  z
87cv 1622 . . . . . . 7  class  z
94cv 1622 . . . . . . 7  class  x
108, 9, 5co 5858 . . . . . 6  class  ( z g x )
11 cgi 20854 . . . . . . 7  class GId
125, 11cfv 5255 . . . . . 6  class  (GId `  g )
1310, 12wceq 1623 . . . . 5  wff  ( z g x )  =  (GId `  g )
1413, 7, 6crio 6297 . . . 4  class  ( iota_ z  e.  ran  g ( z g x )  =  (GId `  g
) )
154, 6, 14cmpt 4077 . . 3  class  ( x  e.  ran  g  |->  (
iota_ z  e.  ran  g ( z g x )  =  (GId
`  g ) ) )
162, 3, 15cmpt 4077 . 2  class  ( g  e.  GrpOp  |->  ( x  e. 
ran  g  |->  ( iota_ z  e.  ran  g ( z g x )  =  (GId `  g
) ) ) )
171, 16wceq 1623 1  wff  inv  =  ( g  e.  GrpOp  |->  ( x  e.  ran  g  |->  ( iota_ z  e. 
ran  g ( z g x )  =  (GId `  g )
) ) )
Colors of variables: wff set class
This definition is referenced by:  grpoinvfval  20891
  Copyright terms: Public domain W3C validator