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

Metamath Proof Explorer

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