This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑅 )
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 ) = 𝑁 )