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

Definition df-minusg 14506
Description: Define inverse of group element. (Contributed by NM, 24-Aug-2011.)
Assertion
Ref Expression
df-minusg  |-  inv g  =  ( g  e. 
_V  |->  ( x  e.  ( Base `  g
)  |->  ( iota_ w  e.  ( Base `  g
) ( w ( +g  `  g ) x )  =  ( 0g `  g ) ) ) )
Distinct variable group:    w, g, x

Detailed syntax breakdown of Definition df-minusg
StepHypRef Expression
1 cminusg 14379 . 2  class  inv g
2 vg . . 3  set  g
3 cvv 2801 . . 3  class  _V
4 vx . . . 4  set  x
52cv 1631 . . . . 5  class  g
6 cbs 13164 . . . . 5  class  Base
75, 6cfv 5271 . . . 4  class  ( Base `  g )
8 vw . . . . . . . 8  set  w
98cv 1631 . . . . . . 7  class  w
104cv 1631 . . . . . . 7  class  x
11 cplusg 13224 . . . . . . . 8  class  +g
125, 11cfv 5271 . . . . . . 7  class  ( +g  `  g )
139, 10, 12co 5874 . . . . . 6  class  ( w ( +g  `  g
) x )
14 c0g 13416 . . . . . . 7  class  0g
155, 14cfv 5271 . . . . . 6  class  ( 0g
`  g )
1613, 15wceq 1632 . . . . 5  wff  ( w ( +g  `  g
) x )  =  ( 0g `  g
)
1716, 8, 7crio 6313 . . . 4  class  ( iota_ w  e.  ( Base `  g
) ( w ( +g  `  g ) x )  =  ( 0g `  g ) )
184, 7, 17cmpt 4093 . . 3  class  ( x  e.  ( Base `  g
)  |->  ( iota_ w  e.  ( Base `  g
) ( w ( +g  `  g ) x )  =  ( 0g `  g ) ) )
192, 3, 18cmpt 4093 . 2  class  ( g  e.  _V  |->  ( x  e.  ( Base `  g
)  |->  ( iota_ w  e.  ( Base `  g
) ( w ( +g  `  g ) x )  =  ( 0g `  g ) ) ) )
201, 19wceq 1632 1  wff  inv g  =  ( g  e. 
_V  |->  ( x  e.  ( Base `  g
)  |->  ( iota_ w  e.  ( Base `  g
) ( w ( +g  `  g ) x )  =  ( 0g `  g ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  grpinvfval  14536
  Copyright terms: Public domain W3C validator