Metamath Proof Explorer

Theorem rhm1

Description: Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015)

Ref Expression
Hypotheses rhm1.o 
|- .1. = ( 1r ` R )
rhm1.n 
|- N = ( 1r ` S )
Assertion rhm1 
|- ( F e. ( R RingHom S ) -> ( F ` .1. ) = N )

Proof

Step Hyp Ref Expression
1 rhm1.o 
 |-  .1. = ( 1r ` R )
2 rhm1.n 
 |-  N = ( 1r ` S )
3 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
4 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
5 3 4 rhmmhm 
 |-  ( F e. ( R RingHom S ) -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
6 eqid 
 |-  ( 0g ` ( mulGrp ` R ) ) = ( 0g ` ( mulGrp ` R ) )
7 eqid 
 |-  ( 0g ` ( mulGrp ` S ) ) = ( 0g ` ( mulGrp ` S ) )
8 6 7 mhm0 
 |-  ( F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) -> ( F ` ( 0g ` ( mulGrp ` R ) ) ) = ( 0g ` ( mulGrp ` S ) ) )
9 5 8 syl 
 |-  ( F e. ( R RingHom S ) -> ( F ` ( 0g ` ( mulGrp ` R ) ) ) = ( 0g ` ( mulGrp ` S ) ) )
10 3 1 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` R ) )
11 10 fveq2i 
 |-  ( F ` .1. ) = ( F ` ( 0g ` ( mulGrp ` R ) ) )
12 4 2 ringidval 
 |-  N = ( 0g ` ( mulGrp ` S ) )
13 9 11 12 3eqtr4g 
 |-  ( F e. ( R RingHom S ) -> ( F ` .1. ) = N )