Theorem lmhmf

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

	Ref	Expression
Hypotheses	lmhmf.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	lmhmf.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
Assertion	lmhmf	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝐵 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		lmhmf.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
2		lmhmf.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
3		lmghm	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
4	1 2	ghmf	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
5	3 4	syl	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝐵 ⟶ 𝐶 )