Metamath Proof Explorer


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