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

Metamath Proof Explorer

Theorem grprinv

Description: The right inverse of a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses grpinv.b 
|- B = ( Base ` G )
grpinv.p 
|- .+ = ( +g ` G )
grpinv.u 
|- .0. = ( 0g ` G )
grpinv.n 
|- N = ( invg ` G )
Assertion grprinv 
|- ( ( G e. Grp /\ X e. B ) -> ( X .+ ( N ` X ) ) = .0. )

Proof

Step Hyp Ref Expression
1 grpinv.b 
 |-  B = ( Base ` G )
2 grpinv.p 
 |-  .+ = ( +g ` G )
3 grpinv.u 
 |-  .0. = ( 0g ` G )
4 grpinv.n 
 |-  N = ( invg ` G )
5 1 2 grpcl 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
6 1 3 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
7 1 2 3 grplid 
 |-  ( ( G e. Grp /\ x e. B ) -> ( .0. .+ x ) = x )
8 1 2 grpass 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
9 1 2 3 grpinvex 
 |-  ( ( G e. Grp /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )
10 simpr 
 |-  ( ( G e. Grp /\ X e. B ) -> X e. B )
11 1 4 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
12 1 2 3 4 grplinv 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ X ) = .0. )
13 5 6 7 8 9 10 11 12 grpinva 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .+ ( N ` X ) ) = .0. )