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	grprinvd	|- ( ( G e. Grp /\ X e. B ) -> ( X .+ ( N ` X ) ) = .0. )