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

Metamath Proof Explorer

Theorem rnghmf

Description: A ring homomorphism is a function. (Contributed by AV, 23-Feb-2020)

Ref Expression
Hypotheses rnghmf.b ⊢ B = Base R
rnghmf.c ⊢ C = Base S
Assertion rnghmf ⊢ F ∈ R RngHom S → F : B ⟶ C

Proof

Step Hyp Ref Expression
1 rnghmf.b ⊢ B = Base R
2 rnghmf.c ⊢ C = Base S
3 rnghmghm ⊢ F ∈ R RngHom S → F ∈ R GrpHom S
4 1 2 ghmf ⊢ F ∈ R GrpHom S → F : B ⟶ C
5 3 4 syl ⊢ F ∈ R RngHom S → F : B ⟶ C