rhm1

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

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

Metamath Proof Explorer