Theorem reldmlmhm

Description: Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014)

	Ref	Expression
Assertion	reldmlmhm	⊢ Rel dom LMHom

Proof

Step	Hyp	Ref	Expression
1		df-lmhm	⊢ LMHom = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
2	1	reldmmpo	⊢ Rel dom LMHom