Theorem reldmlmhm

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

	Ref	Expression
Assertion	reldmlmhm	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{LMHom}$$

Proof

Step	Hyp	Ref	Expression
1		df-lmhm	$$⊢\mathrm{LMHom}=\left(s\in \mathrm{LMod},t\in \mathrm{LMod}⟼\left\{f\in \left(s\mathrm{GrpHom}t\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(s\right)/w\underset{\dot{}}{]}\left(\mathrm{Scalar}\left(t\right)=w\wedge \forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{s}f\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)\right)\right\}\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{LMHom}$$