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

Metamath Proof Explorer

Theorem ghmid

Description: A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Hypotheses ghmid.y 
|- Y = ( 0g ` S )
ghmid.z 
|- .0. = ( 0g ` T )
Assertion ghmid 
|- ( F e. ( S GrpHom T ) -> ( F ` Y ) = .0. )

Proof

Step Hyp Ref Expression
1 ghmid.y 
 |-  Y = ( 0g ` S )
2 ghmid.z 
 |-  .0. = ( 0g ` T )
3 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 4 1 grpidcl 
 |-  ( S e. Grp -> Y e. ( Base ` S ) )
6 3 5 syl 
 |-  ( F e. ( S GrpHom T ) -> Y e. ( Base ` S ) )
7 eqid 
 |-  ( +g ` S ) = ( +g ` S )
8 eqid 
 |-  ( +g ` T ) = ( +g ` T )
9 4 7 8 ghmlin 
 |-  ( ( F e. ( S GrpHom T ) /\ Y e. ( Base ` S ) /\ Y e. ( Base ` S ) ) -> ( F ` ( Y ( +g ` S ) Y ) ) = ( ( F ` Y ) ( +g ` T ) ( F ` Y ) ) )
10 6 6 9 mpd3an23 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( Y ( +g ` S ) Y ) ) = ( ( F ` Y ) ( +g ` T ) ( F ` Y ) ) )
11 4 7 1 grplid 
 |-  ( ( S e. Grp /\ Y e. ( Base ` S ) ) -> ( Y ( +g ` S ) Y ) = Y )
12 3 6 11 syl2anc 
 |-  ( F e. ( S GrpHom T ) -> ( Y ( +g ` S ) Y ) = Y )
13 12 fveq2d 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( Y ( +g ` S ) Y ) ) = ( F ` Y ) )
14 10 13 eqtr3d 
 |-  ( F e. ( S GrpHom T ) -> ( ( F ` Y ) ( +g ` T ) ( F ` Y ) ) = ( F ` Y ) )
15 ghmgrp2 
 |-  ( F e. ( S GrpHom T ) -> T e. Grp )
16 eqid 
 |-  ( Base ` T ) = ( Base ` T )
17 4 16 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
18 17 6 ffvelcdmd 
 |-  ( F e. ( S GrpHom T ) -> ( F ` Y ) e. ( Base ` T ) )
19 16 8 2 grpid 
 |-  ( ( T e. Grp /\ ( F ` Y ) e. ( Base ` T ) ) -> ( ( ( F ` Y ) ( +g ` T ) ( F ` Y ) ) = ( F ` Y ) <-> .0. = ( F ` Y ) ) )
20 15 18 19 syl2anc 
 |-  ( F e. ( S GrpHom T ) -> ( ( ( F ` Y ) ( +g ` T ) ( F ` Y ) ) = ( F ` Y ) <-> .0. = ( F ` Y ) ) )
21 14 20 mpbid 
 |-  ( F e. ( S GrpHom T ) -> .0. = ( F ` Y ) )
22 21 eqcomd 
 |-  ( F e. ( S GrpHom T ) -> ( F ` Y ) = .0. )