Metamath Proof Explorer

Theorem ringidval

Description: The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses ringidval.g 
|- G = ( mulGrp ` R )
ringidval.u 
|- .1. = ( 1r ` R )
Assertion ringidval 
|- .1. = ( 0g ` G )

Proof

Step Hyp Ref Expression
1 ringidval.g 
 |-  G = ( mulGrp ` R )
2 ringidval.u 
 |-  .1. = ( 1r ` R )
3 df-ur 
 |-  1r = ( 0g o. mulGrp )
4 3 fveq1i 
 |-  ( 1r ` R ) = ( ( 0g o. mulGrp ) ` R )
5 fnmgp 
 |-  mulGrp Fn _V
6 fvco2 
 |-  ( ( mulGrp Fn _V /\ R e. _V ) -> ( ( 0g o. mulGrp ) ` R ) = ( 0g ` ( mulGrp ` R ) ) )
7 5 6 mpan 
 |-  ( R e. _V -> ( ( 0g o. mulGrp ) ` R ) = ( 0g ` ( mulGrp ` R ) ) )
8 4 7 syl5eq 
 |-  ( R e. _V -> ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) ) )
9 0g0 
 |-  (/) = ( 0g ` (/) )
10 fvprc 
 |-  ( -. R e. _V -> ( 1r ` R ) = (/) )
11 fvprc 
 |-  ( -. R e. _V -> ( mulGrp ` R ) = (/) )
12 11 fveq2d 
 |-  ( -. R e. _V -> ( 0g ` ( mulGrp ` R ) ) = ( 0g ` (/) ) )
13 9 10 12 3eqtr4a 
 |-  ( -. R e. _V -> ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) ) )
14 8 13 pm2.61i 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
15 1 fveq2i 
 |-  ( 0g ` G ) = ( 0g ` ( mulGrp ` R ) )
16 14 2 15 3eqtr4i 
 |-  .1. = ( 0g ` G )