Theorem reldmnmhm

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

	Ref	Expression
Assertion	reldmnmhm	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{NMHom}$$

Proof

Step	Hyp	Ref	Expression
1		df-nmhm	$$⊢\mathrm{NMHom}=\left(s\in \mathrm{NrmMod},t\in \mathrm{NrmMod}⟼\left(s\mathrm{LMHom}t\right)\cap \left(s\mathrm{NGHom}t\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{NMHom}$$