Theorem rhm1

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

	Ref	Expression
Hypotheses	rhm1.o	$$⊢\underset{\dot{}}{1}=1_R$$
	rhm1.n	$$⊢N=1_S$$
Assertion	rhm1	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\left(\underset{\dot{}}{1}\right)=N$$

Proof

Step	Hyp	Ref	Expression
1		rhm1.o	$$⊢\underset{\dot{}}{1}=1_R$$
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	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
11	10	fveq2i	$$⊢F\left(\underset{\dot{}}{1}\right)=F\left(0_{{\mathrm{mulGrp}}_R}\right)$$
12	4 2	ringidval	$$⊢N=0_{{\mathrm{mulGrp}}_S}$$
13	9 11 12	3eqtr4g	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\left(\underset{\dot{}}{1}\right)=N$$