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

Definition df-gdiv 20861
Description: Define a function that maps a group operation to the group's division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-gdiv  |-  /g  =  ( g  e.  GrpOp  |->  ( x  e.  ran  g ,  y  e.  ran  g  |->  ( x g ( ( inv `  g ) `  y
) ) ) )
Distinct variable group:    x, g, y

Detailed syntax breakdown of Definition df-gdiv
StepHypRef Expression
1 cgs 20856 . 2  class  /g
2 vg . . 3  set  g
3 cgr 20853 . . 3  class  GrpOp
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1622 . . . . 5  class  g
76crn 4690 . . . 4  class  ran  g
84cv 1622 . . . . 5  class  x
95cv 1622 . . . . . 6  class  y
10 cgn 20855 . . . . . . 7  class  inv
116, 10cfv 5255 . . . . . 6  class  ( inv `  g )
129, 11cfv 5255 . . . . 5  class  ( ( inv `  g ) `
 y )
138, 12, 6co 5858 . . . 4  class  ( x g ( ( inv `  g ) `  y
) )
144, 5, 7, 7, 13cmpt2 5860 . . 3  class  ( x  e.  ran  g ,  y  e.  ran  g  |->  ( x g ( ( inv `  g
) `  y )
) )
152, 3, 14cmpt 4077 . 2  class  ( g  e.  GrpOp  |->  ( x  e. 
ran  g ,  y  e.  ran  g  |->  ( x g ( ( inv `  g ) `
 y ) ) ) )
161, 15wceq 1623 1  wff  /g  =  ( g  e.  GrpOp  |->  ( x  e.  ran  g ,  y  e.  ran  g  |->  ( x g ( ( inv `  g ) `  y
) ) ) )
Colors of variables: wff set class
This definition is referenced by:  grpodivfval  20909  vsfval  21191
  Copyright terms: Public domain W3C validator