Theorem ghmid

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

	Ref	Expression
Hypotheses	ghmid.y	$$⊢Y=0_S$$
	ghmid.z	$$⊢\underset{\dot{}}{0}=0_T$$
Assertion	ghmid	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\left(Y\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		ghmid.y	$$⊢Y=0_S$$
2		ghmid.z	$$⊢\underset{\dot{}}{0}=0_T$$
3		ghmgrp1	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to S\in \mathrm{Grp}$$
4		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
5	4 1	grpidcl	$$⊢S\in \mathrm{Grp}\to Y\in {\mathrm{Base}}_S$$
6	3 5	syl	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to Y\in {\mathrm{Base}}_S$$
7		eqid	$$⊢{+}_S={+}_S$$
8		eqid	$$⊢{+}_T={+}_T$$
9	4 7 8	ghmlin	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge Y\in {\mathrm{Base}}_S\wedge Y\in {\mathrm{Base}}_S\right)\to F\left(Y{+}_{S}Y\right)=F\left(Y\right){+}_{T}F\left(Y\right)$$
10	6 6 9	mpd3an23	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\left(Y{+}_{S}Y\right)=F\left(Y\right){+}_{T}F\left(Y\right)$$
11	4 7 1	grplid	$$⊢\left(S\in \mathrm{Grp}\wedge Y\in {\mathrm{Base}}_S\right)\to Y{+}_{S}Y=Y$$
12	3 6 11	syl2anc	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to Y{+}_{S}Y=Y$$
13	12	fveq2d	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\left(Y{+}_{S}Y\right)=F\left(Y\right)$$
14	10 13	eqtr3d	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\left(Y\right){+}_{T}F\left(Y\right)=F\left(Y\right)$$
15		ghmgrp2	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to T\in \mathrm{Grp}$$
16		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
17	4 16	ghmf	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T$$
18	17 6	ffvelrnd	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\left(Y\right)\in {\mathrm{Base}}_T$$
19	16 8 2	grpid	$$⊢\left(T\in \mathrm{Grp}\wedge F\left(Y\right)\in {\mathrm{Base}}_T\right)\to \left(F\left(Y\right){+}_{T}F\left(Y\right)=F\left(Y\right)\leftrightarrow \underset{\dot{}}{0}=F\left(Y\right)\right)$$
20	15 18 19	syl2anc	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to \left(F\left(Y\right){+}_{T}F\left(Y\right)=F\left(Y\right)\leftrightarrow \underset{\dot{}}{0}=F\left(Y\right)\right)$$
21	14 20	mpbid	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to \underset{\dot{}}{0}=F\left(Y\right)$$
22	21	eqcomd	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\left(Y\right)=\underset{\dot{}}{0}$$