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

Metamath Proof Explorer

Theorem rnghmmgmhm

Description: A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses isrnghmmul.m ⊢ M = mulGrp R
isrnghmmul.n ⊢ N = mulGrp S
Assertion rnghmmgmhm ⊢ F ∈ R RngHom S → F ∈ M MgmHom N

Proof

Step Hyp Ref Expression
1 isrnghmmul.m ⊢ M = mulGrp R
2 isrnghmmul.n ⊢ N = mulGrp S
3 1 2 isrnghmmul ⊢ F ∈ R RngHom S ↔ R ∈ Rng ∧ S ∈ Rng ∧ F ∈ R GrpHom S ∧ F ∈ M MgmHom N
4 3 simprbi ⊢ F ∈ R RngHom S → F ∈ R GrpHom S ∧ F ∈ M MgmHom N
5 4 simprd ⊢ F ∈ R RngHom S → F ∈ M MgmHom N