Theorem 0ghm

Description: The constant zero linear function between two groups. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	0ghm.z	|- .0. = ( 0g ` N )
	0ghm.b	|- B = ( Base ` M )
Assertion	0ghm	|- ( ( M e. Grp /\ N e. Grp ) -> ( B X. { .0. } ) e. ( M GrpHom N ) )

Proof

Step	Hyp	Ref	Expression
1		0ghm.z	|- .0. = ( 0g ` N )
2		0ghm.b	|- B = ( Base ` M )
3		grpmnd	|- ( M e. Grp -> M e. Mnd )
4		grpmnd	|- ( N e. Grp -> N e. Mnd )
5	1 2	0mhm	|- ( ( M e. Mnd /\ N e. Mnd ) -> ( B X. { .0. } ) e. ( M MndHom N ) )
6	3 4 5	syl2an	|- ( ( M e. Grp /\ N e. Grp ) -> ( B X. { .0. } ) e. ( M MndHom N ) )
7		ghmmhmb	|- ( ( M e. Grp /\ N e. Grp ) -> ( M GrpHom N ) = ( M MndHom N ) )
8	6 7	eleqtrrd	|- ( ( M e. Grp /\ N e. Grp ) -> ( B X. { .0. } ) e. ( M GrpHom N ) )