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 ‘ 𝑅 )
	rhm1.n	⊢ 𝑁 = ( 1r ‘ 𝑆 )
Assertion	rhm1	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ 1 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		rhm1.o	⊢ 1 = ( 1r ‘ 𝑅 )
2		rhm1.n	⊢ 𝑁 = ( 1r ‘ 𝑆 )
3		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
4		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
5	3 4	rhmmhm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) )
6		eqid	⊢ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
7		eqid	⊢ ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) )
8	6 7	mhm0	⊢ ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) )
9	5 8	syl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) ) )
10	3 1	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
11	10	fveq2i	⊢ ( 𝐹 ‘ 1 ) = ( 𝐹 ‘ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
12	4 2	ringidval	⊢ 𝑁 = ( 0g ‘ ( mulGrp ‘ 𝑆 ) )
13	9 11 12	3eqtr4g	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ 1 ) = 𝑁 )