Metamath Proof Explorer

Theorem reldmfrlm

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

Ref Expression
Assertion reldmfrlm 
|- Rel dom freeLMod

Proof

Step Hyp Ref Expression
1 df-frlm 
 |-  freeLMod = ( r e. _V , i e. _V |-> ( r (+)m ( i X. { ( ringLMod ` r ) } ) ) )
2 1 reldmmpo 
 |-  Rel dom freeLMod