Theorem ghmker

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

	Ref	Expression
Hypothesis	ghmker.1	$$⊢\underset{\dot{}}{0}=0_T$$
Assertion	ghmker	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{NrmSGrp}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		ghmker.1	$$⊢\underset{\dot{}}{0}=0_T$$
2		ghmgrp2	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to T\in \mathrm{Grp}$$
3	1	0nsg	$$⊢T\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{NrmSGrp}\left(T\right)$$
4	2 3	syl	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{NrmSGrp}\left(T\right)$$
5		ghmnsgpreima	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge \left\{\underset{\dot{}}{0}\right\}\in \mathrm{NrmSGrp}\left(T\right)\right)\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{NrmSGrp}\left(S\right)$$
6	4 5	mpdan	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{NrmSGrp}\left(S\right)$$