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	ffvelrnd	|- ( 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. )