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

Metamath Proof Explorer

Theorem rnghmghm

Description: A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020)

Ref Expression
Assertion rnghmghm ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
3 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
4 1 2 3 isrnghm ⊢ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
5 simprl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
6 4 5 sylbi ⊢ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )