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. ) )