Theorem reldmfrlm

Description: The domain of the free module function is a relation. (Contributed by SN, 24-Sep-2026)

	Ref	Expression
Assertion	reldmfrlm	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{freeLMod}$$

Proof

Step	Hyp	Ref	Expression
1		df-frlm	$$⊢\mathrm{freeLMod}=\left(r\in \mathrm{V},i\in \mathrm{V}⟼r{\oplus }_m\left(i\times \left\{\mathrm{ringLMod}\left(r\right)\right\}\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{freeLMod}$$