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 ` T )
Assertion	ghmker	|- ( F e. ( S GrpHom T ) -> ( `' F " { .0. } ) e. ( NrmSGrp ` S ) )

Proof

Step	Hyp	Ref	Expression
1		ghmker.1	|- .0. = ( 0g ` T )
2		ghmgrp2	|- ( F e. ( S GrpHom T ) -> T e. Grp )
3	1	0nsg	|- ( T e. Grp -> { .0. } e. ( NrmSGrp ` T ) )
4	2 3	syl	|- ( F e. ( S GrpHom T ) -> { .0. } e. ( NrmSGrp ` T ) )
5		ghmnsgpreima	|- ( ( F e. ( S GrpHom T ) /\ { .0. } e. ( NrmSGrp ` T ) ) -> ( `' F " { .0. } ) e. ( NrmSGrp ` S ) )
6	4 5	mpdan	|- ( F e. ( S GrpHom T ) -> ( `' F " { .0. } ) e. ( NrmSGrp ` S ) )