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. = ( 0g ` S )
zrrhm.h
|- H = ( x e. B |-> .0. )
c0snmhm.z
|- Z = ( 0g ` T )
Assertion c0snghm
|- ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> H e. ( T GrpHom S ) )

Proof

Step Hyp Ref Expression
1 zrrhm.b
 |-  B = ( Base ` T )
2 zrrhm.0
 |-  .0. = ( 0g ` S )
3 zrrhm.h
 |-  H = ( x e. B |-> .0. )
4 c0snmhm.z
 |-  Z = ( 0g ` T )
5 grpmnd
 |-  ( S e. Grp -> S e. Mnd )
6 grpmnd
 |-  ( T e. Grp -> T e. Mnd )
7 id
 |-  ( B = { Z } -> B = { Z } )
8 1 2 3 4 c0snmhm
 |-  ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H e. ( T MndHom S ) )
9 5 6 7 8 syl3an
 |-  ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> H e. ( T MndHom S ) )
10 ghmmhmb
 |-  ( ( T e. Grp /\ S e. Grp ) -> ( T GrpHom S ) = ( T MndHom S ) )
11 10 eleq2d
 |-  ( ( T e. Grp /\ S e. Grp ) -> ( H e. ( T GrpHom S ) <-> H e. ( T MndHom S ) ) )
12 11 ancoms
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( H e. ( T GrpHom S ) <-> H e. ( T MndHom S ) ) )
13 12 3adant3
 |-  ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> ( H e. ( T GrpHom S ) <-> H e. ( T MndHom S ) ) )
14 9 13 mpbird
 |-  ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> H e. ( T GrpHom S ) )