This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )