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 ⊢ 𝑌 = ( 0g ‘ 𝑆 )
ghmid.z ⊢ 0 = ( 0g ‘ 𝑇 )
Assertion ghmid ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ 𝑌 ) = 0 )

Proof

Step Hyp Ref Expression
1 ghmid.y ⊢ 𝑌 = ( 0g ‘ 𝑆 )
2 ghmid.z ⊢ 0 = ( 0g ‘ 𝑇 )
3 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
4 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5 4 1 grpidcl ⊢ ( 𝑆 ∈ Grp → 𝑌 ∈ ( Base ‘ 𝑆 ) )
6 3 5 syl ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑌 ∈ ( Base ‘ 𝑆 ) )
7 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
8 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
9 4 7 8 ghmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑌 ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑌 ( +g ‘ 𝑆 ) 𝑌 ) ) = ( ( 𝐹 ‘ 𝑌 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑌 ) ) )
10 6 6 9 mpd3an23 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ ( 𝑌 ( +g ‘ 𝑆 ) 𝑌 ) ) = ( ( 𝐹 ‘ 𝑌 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑌 ) ) )
11 4 7 1 grplid ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑌 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑌 ( +g ‘ 𝑆 ) 𝑌 ) = 𝑌 )
12 3 6 11 syl2anc ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝑌 ( +g ‘ 𝑆 ) 𝑌 ) = 𝑌 )
13 12 fveq2d ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ ( 𝑌 ( +g ‘ 𝑆 ) 𝑌 ) ) = ( 𝐹 ‘ 𝑌 ) )
14 10 13 eqtr3d ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( ( 𝐹 ‘ 𝑌 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ 𝑌 ) )
15 ghmgrp2 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑇 ∈ Grp )
16 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
17 4 16 ghmf ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
18 17 6 ffvelcdmd ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝑇 ) )
19 16 8 2 grpid ⊢ ( ( 𝑇 ∈ Grp ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( ( 𝐹 ‘ 𝑌 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ 𝑌 ) ↔ 0 = ( 𝐹 ‘ 𝑌 ) ) )
20 15 18 19 syl2anc ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( ( ( 𝐹 ‘ 𝑌 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ 𝑌 ) ↔ 0 = ( 𝐹 ‘ 𝑌 ) ) )
21 14 20 mpbid ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 0 = ( 𝐹 ‘ 𝑌 ) )
22 21 eqcomd ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ 𝑌 ) = 0 )