Theorem grpoinvfval

Description: The inverse function of a group. (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	grpoinvfval	|- ( G e. GrpOp -> N = ( x e. X |-> ( iota_ y e. X ( y G x ) = 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		rnexg	|- ( G e. GrpOp -> ran G e. _V )
5	1 4	eqeltrid	|- ( G e. GrpOp -> X e. _V )
6		mptexg	|- ( X e. _V -> ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) e. _V )
7	5 6	syl	|- ( G e. GrpOp -> ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) e. _V )
8		rneq	|- ( g = G -> ran g = ran G )
9	8 1	eqtr4di	|- ( g = G -> ran g = X )
10		oveq	|- ( g = G -> ( y g x ) = ( y G x ) )
11		fveq2	|- ( g = G -> ( GId ` g ) = ( GId ` G ) )
12	11 2	eqtr4di	|- ( g = G -> ( GId ` g ) = U )
13	10 12	eqeq12d	|- ( g = G -> ( ( y g x ) = ( GId ` g ) <-> ( y G x ) = U ) )
14	9 13	riotaeqbidv	|- ( g = G -> ( iota_ y e. ran g ( y g x ) = ( GId ` g ) ) = ( iota_ y e. X ( y G x ) = U ) )
15	9 14	mpteq12dv	|- ( g = G -> ( x e. ran g |-> ( iota_ y e. ran g ( y g x ) = ( GId ` g ) ) ) = ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) )
16		df-ginv	|- inv = ( g e. GrpOp |-> ( x e. ran g |-> ( iota_ y e. ran g ( y g x ) = ( GId ` g ) ) ) )
17	15 16	fvmptg	|- ( ( G e. GrpOp /\ ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) e. _V ) -> ( inv ` G ) = ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) )
18	7 17	mpdan	|- ( G e. GrpOp -> ( inv ` G ) = ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) )
19	3 18	eqtrid	|- ( G e. GrpOp -> N = ( x e. X |-> ( iota_ y e. X ( y G x ) = U ) ) )