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

Metamath Proof Explorer

Theorem c0ghm

Description: The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020)

Ref Expression
Hypotheses c0mhm.b 
|- B = ( Base ` S )
c0mhm.0 
|- .0. = ( 0g ` T )
c0mhm.h 
|- H = ( x e. B |-> .0. )
Assertion c0ghm 
|- ( ( S e. Grp /\ T e. Grp ) -> H e. ( S GrpHom T ) )

Proof

Step Hyp Ref Expression
1 c0mhm.b 
 |-  B = ( Base ` S )
2 c0mhm.0 
 |-  .0. = ( 0g ` T )
3 c0mhm.h 
 |-  H = ( x e. B |-> .0. )
4 grpmnd 
 |-  ( S e. Grp -> S e. Mnd )
5 grpmnd 
 |-  ( T e. Grp -> T e. Mnd )
6 4 5 anim12i 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( S e. Mnd /\ T e. Mnd ) )
7 1 2 3 c0mhm 
 |-  ( ( S e. Mnd /\ T e. Mnd ) -> H e. ( S MndHom T ) )
8 6 7 syl 
 |-  ( ( S e. Grp /\ T e. Grp ) -> H e. ( S MndHom T ) )
9 ghmmhmb 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( S GrpHom T ) = ( S MndHom T ) )
10 9 eleq2d 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( H e. ( S GrpHom T ) <-> H e. ( S MndHom T ) ) )
11 8 10 mpbird 
 |-  ( ( S e. Grp /\ T e. Grp ) -> H e. ( S GrpHom T ) )