Theorem ghmker

Description: The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypothesis	ghmker.1	⊢ 0 = ( 0g ‘ 𝑇 )
Assertion	ghmker	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( NrmSGrp ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		ghmker.1	⊢ 0 = ( 0g ‘ 𝑇 )
2		ghmgrp2	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑇 ∈ Grp )
3	1	0nsg	⊢ ( 𝑇 ∈ Grp → { 0 } ∈ ( NrmSGrp ‘ 𝑇 ) )
4	2 3	syl	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → { 0 } ∈ ( NrmSGrp ‘ 𝑇 ) )
5		ghmnsgpreima	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ { 0 } ∈ ( NrmSGrp ‘ 𝑇 ) ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( NrmSGrp ‘ 𝑆 ) )
6	4 5	mpdan	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( NrmSGrp ‘ 𝑆 ) )