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

Metamath Proof Explorer

Theorem gidval

Description: The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis gidval.1 
|- X = ran G
Assertion gidval 
|- ( G e. V -> ( GId ` G ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )

Proof

Step Hyp Ref Expression
1 gidval.1 
 |-  X = ran G
2 elex 
 |-  ( G e. V -> G e. _V )
3 rneq 
 |-  ( g = G -> ran g = ran G )
4 3 1 eqtr4di 
 |-  ( g = G -> ran g = X )
5 oveq 
 |-  ( g = G -> ( u g x ) = ( u G x ) )
6 5 eqeq1d 
 |-  ( g = G -> ( ( u g x ) = x <-> ( u G x ) = x ) )
7 oveq 
 |-  ( g = G -> ( x g u ) = ( x G u ) )
8 7 eqeq1d 
 |-  ( g = G -> ( ( x g u ) = x <-> ( x G u ) = x ) )
9 6 8 anbi12d 
 |-  ( g = G -> ( ( ( u g x ) = x /\ ( x g u ) = x ) <-> ( ( u G x ) = x /\ ( x G u ) = x ) ) )
10 4 9 raleqbidv 
 |-  ( g = G -> ( A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) <-> A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
11 4 10 riotaeqbidv 
 |-  ( g = G -> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
12 df-gid 
 |-  GId = ( g e. _V |-> ( iota_ u e. ran g A. x e. ran g ( ( u g x ) = x /\ ( x g u ) = x ) ) )
13 riotaex 
 |-  ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) e. _V
14 11 12 13 fvmpt 
 |-  ( G e. _V -> ( GId ` G ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
15 2 14 syl 
 |-  ( G e. V -> ( GId ` G ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )