This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-minusg

Description: Define inverse of group element. (Contributed by NM, 24-Aug-2011)

Ref Expression
Assertion df-minusg 
|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminusg 
 |-  invg
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( Base ` g )
7 vw 
 |-  w
8 7 cv 
 |-  w
9 cplusg 
 |-  +g
10 5 9 cfv 
 |-  ( +g ` g )
11 3 cv 
 |-  x
12 8 11 10 co 
 |-  ( w ( +g ` g ) x )
13 c0g 
 |-  0g
14 5 13 cfv 
 |-  ( 0g ` g )
15 12 14 wceq 
 |-  ( w ( +g ` g ) x ) = ( 0g ` g )
16 15 7 6 crio 
 |-  ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) )
17 3 6 16 cmpt 
 |-  ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) )
18 1 2 17 cmpt 
 |-  ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
19 0 18 wceq 
 |-  invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )