Metamath Proof Explorer

Theorem rhmisrnghm

Description: Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020)

Ref Expression
Assertion rhmisrnghm ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ringrng ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
2 ringrng ⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Rng )
3 1 2 anim12i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) )
4 mhmismgmhm ⊢ ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑆 ) ) )
5 4 anim2i ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑆 ) ) ) )
6 3 5 anim12i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ) → ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑆 ) ) ) ) )
7 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
8 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
9 7 8 isrhm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ) )
10 7 8 isrnghmmul ⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MgmHom ( mulGrp ‘ 𝑆 ) ) ) ) )
11 6 9 10 3imtr4i ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) )