Description: Lemma for module homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | reldmlmhm | ⊢ Rel dom LMHom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-lmhm | ⊢ LMHom = ( 𝑠 ∈ LMod , 𝑡 ∈ LMod ↦ { 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ [ ( Scalar ‘ 𝑠 ) / 𝑤 ] ( ( Scalar ‘ 𝑡 ) = 𝑤 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑤 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑠 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ) } ) | |
2 | 1 | reldmmpo | ⊢ Rel dom LMHom |