Theorem grpoinvval

Description: The inverse of a group element. (Contributed by NM, 26-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpinvfval.1	|- X = ran G
	grpinvfval.2	|- U = ( GId ` G )
	grpinvfval.3	|- N = ( inv ` G )
Assertion	grpoinvval	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) = ( iota_ y e. X ( y G A ) = U ) )

Proof

Step	Hyp	Ref	Expression
1		grpinvfval.1	|- X = ran G
2		grpinvfval.2	|- U = ( GId ` G )
3		grpinvfval.3	|- N = ( inv ` G )
4	1 2 3	grpoinvfval	|- ( G e. GrpOp -> N = ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) )
5	4	fveq1d	|- ( G e. GrpOp -> ( N ` A ) = ( ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) ` A ) )
6		oveq2	|- ( x = A -> ( y G x ) = ( y G A ) )
7	6	eqeq1d	|- ( x = A -> ( ( y G x ) = U <-> ( y G A ) = U ) )
8	7	riotabidv	|- ( x = A -> ( iota_ y e. X ( y G x ) = U ) = ( iota_ y e. X ( y G A ) = U ) )
9		eqid	|- ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) = ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) )
10		riotaex	|- ( iota_ y e. X ( y G A ) = U ) e. _V
11	8 9 10	fvmpt	|- ( A e. X -> ( ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) ` A ) = ( iota_ y e. X ( y G A ) = U ) )
12	5 11	sylan9eq	|- ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) = ( iota_ y e. X ( y G A ) = U ) )