Theorem reldmnmhm

Description: Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015)

	Ref	Expression
Assertion	reldmnmhm	⊢ Rel dom NMHom

Proof

Step	Hyp	Ref	Expression
1		df-nmhm	⊢ NMHom = ( 𝑠 ∈ NrmMod , 𝑡 ∈ NrmMod ↦ ( ( 𝑠 LMHom 𝑡 ) ∩ ( 𝑠 NGHom 𝑡 ) ) )
2	1	reldmmpo	⊢ Rel dom NMHom