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

Metamath Proof Explorer

Theorem grpinvval

Description: The inverse of a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 7-Aug-2013)

Ref Expression
Hypotheses grpinvval.b 
|- B = ( Base ` G )
grpinvval.p 
|- .+ = ( +g ` G )
grpinvval.o 
|- .0. = ( 0g ` G )
grpinvval.n 
|- N = ( invg ` G )
Assertion grpinvval 
|- ( X e. B -> ( N ` X ) = ( iota_ y e. B ( y .+ X ) = .0. ) )

Proof

Step Hyp Ref Expression
1 grpinvval.b 
 |-  B = ( Base ` G )
2 grpinvval.p 
 |-  .+ = ( +g ` G )
3 grpinvval.o 
 |-  .0. = ( 0g ` G )
4 grpinvval.n 
 |-  N = ( invg ` G )
5 oveq2 
 |-  ( x = X -> ( y .+ x ) = ( y .+ X ) )
6 5 eqeq1d 
 |-  ( x = X -> ( ( y .+ x ) = .0. <-> ( y .+ X ) = .0. ) )
7 6 riotabidv 
 |-  ( x = X -> ( iota_ y e. B ( y .+ x ) = .0. ) = ( iota_ y e. B ( y .+ X ) = .0. ) )
8 1 2 3 4 grpinvfval 
 |-  N = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) )
9 riotaex 
 |-  ( iota_ y e. B ( y .+ X ) = .0. ) e. _V
10 7 8 9 fvmpt 
 |-  ( X e. B -> ( N ` X ) = ( iota_ y e. B ( y .+ X ) = .0. ) )