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