Metamath Proof Explorer


Theorem c0snghm

Description: The constant mapping to zero is a group homomorphism from the trivial group (consisting of the zero only) to any group. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrrhm.b B = Base T
zrrhm.0 0 ˙ = 0 S
zrrhm.h H = x B 0 ˙
c0snmhm.z Z = 0 T
Assertion c0snghm S Grp T Grp B = Z H T GrpHom S

Proof

Step Hyp Ref Expression
1 zrrhm.b B = Base T
2 zrrhm.0 0 ˙ = 0 S
3 zrrhm.h H = x B 0 ˙
4 c0snmhm.z Z = 0 T
5 grpmnd S Grp S Mnd
6 grpmnd T Grp T Mnd
7 id B = Z B = Z
8 1 2 3 4 c0snmhm S Mnd T Mnd B = Z H T MndHom S
9 5 6 7 8 syl3an S Grp T Grp B = Z H T MndHom S
10 ghmmhmb T Grp S Grp T GrpHom S = T MndHom S
11 10 eleq2d T Grp S Grp H T GrpHom S H T MndHom S
12 11 ancoms S Grp T Grp H T GrpHom S H T MndHom S
13 12 3adant3 S Grp T Grp B = Z H T GrpHom S H T MndHom S
14 9 13 mpbird S Grp T Grp B = Z H T GrpHom S