Metamath Proof Explorer

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 = ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) )
2 1 reldmmpo 
 |-  Rel dom NMHom