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

Metamath Proof Explorer

Theorem lmhmf

Description: A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Hypotheses lmhmf.b ⊢ B = Base S
lmhmf.c ⊢ C = Base T
Assertion lmhmf ⊢ F ∈ S LMHom T → F : B ⟶ C

Proof

Step Hyp Ref Expression
1 lmhmf.b ⊢ B = Base S
2 lmhmf.c ⊢ C = Base T
3 lmghm ⊢ F ∈ S LMHom T → F ∈ S GrpHom T
4 1 2 ghmf ⊢ F ∈ S GrpHom T → F : B ⟶ C
5 3 4 syl ⊢ F ∈ S LMHom T → F : B ⟶ C