# 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 = 0 S$
ghmid.z
Assertion ghmid

### Proof

Step Hyp Ref Expression
1 ghmid.y $⊢ Y = 0 S$
2 ghmid.z
3 ghmgrp1 $⊢ F ∈ S GrpHom T → S ∈ Grp$
4 eqid $⊢ Base S = Base S$
5 4 1 grpidcl $⊢ S ∈ Grp → Y ∈ Base S$
6 3 5 syl $⊢ F ∈ S GrpHom T → Y ∈ Base S$
7 eqid $⊢ + S = + S$
8 eqid $⊢ + T = + T$
9 4 7 8 ghmlin $⊢ F ∈ S GrpHom T ∧ Y ∈ Base S ∧ Y ∈ Base S → F ⁡ Y + S Y = F ⁡ Y + T F ⁡ Y$
10 6 6 9 mpd3an23 $⊢ F ∈ S GrpHom T → F ⁡ Y + S Y = F ⁡ Y + T F ⁡ Y$
11 4 7 1 grplid $⊢ S ∈ Grp ∧ Y ∈ Base S → Y + S Y = Y$
12 3 6 11 syl2anc $⊢ F ∈ S GrpHom T → Y + S Y = Y$
13 12 fveq2d $⊢ F ∈ S GrpHom T → F ⁡ Y + S Y = F ⁡ Y$
14 10 13 eqtr3d $⊢ F ∈ S GrpHom T → F ⁡ Y + T F ⁡ Y = F ⁡ Y$
15 ghmgrp2 $⊢ F ∈ S GrpHom T → T ∈ Grp$
16 eqid $⊢ Base T = Base T$
17 4 16 ghmf $⊢ F ∈ S GrpHom T → F : Base S ⟶ Base T$
18 17 6 ffvelrnd $⊢ F ∈ S GrpHom T → F ⁡ Y ∈ Base T$
19 16 8 2 grpid
20 15 18 19 syl2anc
21 14 20 mpbid
22 21 eqcomd