0ghm

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

	Ref	Expression
Hypotheses	0ghm.z	$⊢ \underset{˙}{0} = 0_{N}$
	0ghm.b	$⊢ B = {Base}_{M}$
Assertion	0ghm	$⊢ (M \in Grp \land N \in Grp) \to B \times \{\underset{˙}{0}\} \in (M GrpHom N)$

Step	Hyp	Ref	Expression
1		0ghm.z	$⊢ \underset{˙}{0} = 0_{N}$
2		0ghm.b	$⊢ B = {Base}_{M}$
3		grpmnd	$⊢ M \in Grp \to M \in Mnd$
4		grpmnd	$⊢ N \in Grp \to N \in Mnd$
5	1 2	0mhm	$⊢ (M \in Mnd \land N \in Mnd) \to B \times \{\underset{˙}{0}\} \in (M MndHom N)$
6	3 4 5	syl2an	$⊢ (M \in Grp \land N \in Grp) \to B \times \{\underset{˙}{0}\} \in (M MndHom N)$
7		ghmmhmb	$⊢ (M \in Grp \land N \in Grp) \to M GrpHom N = M MndHom N$
8	6 7	eleqtrrd	$⊢ (M \in Grp \land N \in Grp) \to B \times \{\underset{˙}{0}\} \in (M GrpHom N)$

Metamath Proof Explorer