Metamath Proof Explorer

Theorem reldmghm

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

		Ref	Expression
	Assertion	reldmghm	\|- Rel dom GrpHom

Proof

Step	Hyp	Ref	Expression
1		df-ghm	\|- GrpHom = ( s e. Grp , t e. Grp \|-> { g \| [. ( Base ` s ) / w ]. ( g : w --> ( Base ` t ) /\ A. x e. w A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) ) ) } )
2	1	reldmmpo	\|- Rel dom GrpHom

Step

Hyp

Ref

Expression

df-ghm

 |-  GrpHom = ( s e. Grp , t e. Grp |-> { g | [. ( Base ` s ) / w ]. ( g : w --> ( Base ` t ) /\ A. x e. w A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) ) ) } )

reldmmpo

 |-  Rel dom GrpHom