# 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
rhm1.n ${⊢}{N}={1}_{{S}}$
Assertion rhm1

### Proof

Step Hyp Ref Expression
1 rhm1.o
2 rhm1.n ${⊢}{N}={1}_{{S}}$
3 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
4 eqid ${⊢}{\mathrm{mulGrp}}_{{S}}={\mathrm{mulGrp}}_{{S}}$
5 3 4 rhmmhm ${⊢}{F}\in \left({R}\mathrm{RingHom}{S}\right)\to {F}\in \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)$
6 eqid ${⊢}{0}_{{\mathrm{mulGrp}}_{{R}}}={0}_{{\mathrm{mulGrp}}_{{R}}}$
7 eqid ${⊢}{0}_{{\mathrm{mulGrp}}_{{S}}}={0}_{{\mathrm{mulGrp}}_{{S}}}$
8 6 7 mhm0 ${⊢}{F}\in \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\to {F}\left({0}_{{\mathrm{mulGrp}}_{{R}}}\right)={0}_{{\mathrm{mulGrp}}_{{S}}}$
9 5 8 syl ${⊢}{F}\in \left({R}\mathrm{RingHom}{S}\right)\to {F}\left({0}_{{\mathrm{mulGrp}}_{{R}}}\right)={0}_{{\mathrm{mulGrp}}_{{S}}}$
10 3 1 ringidval
11 10 fveq2i
12 4 2 ringidval ${⊢}{N}={0}_{{\mathrm{mulGrp}}_{{S}}}$
13 9 11 12 3eqtr4g