Metamath Proof Explorer

Theorem reldmlmhm

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

		Ref	Expression
	Assertion	reldmlmhm	\|- Rel dom LMHom

Proof

Step	Hyp	Ref	Expression
1		df-lmhm	\|- LMHom = ( s e. LMod , t e. LMod \|-> { f e. ( s GrpHom t ) \| [. ( Scalar ` s ) / w ]. ( ( Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) } )
2	1	reldmmpo	\|- Rel dom LMHom

Step

Hyp

Ref

Expression

df-lmhm

 |-  LMHom = ( s e. LMod , t e. LMod |-> { f e. ( s GrpHom t ) | [. ( Scalar ` s ) / w ]. ( ( Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) ) } )

reldmmpo

 |-  Rel dom LMHom