cntrnsg

Description: The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015)

		Ref	Expression
	Hypothesis	cntrnsg.z	$⊢ Z = Cntr (M)$
	Assertion	cntrnsg	$⊢ M \in Grp \to Z \in NrmSGrp (M)$

Step	Hyp	Ref	Expression
1		cntrnsg.z	$⊢ Z = Cntr (M)$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3		eqid	$⊢ Cntz (M) = Cntz (M)$
4	2 3	cntrval	$⊢ Cntz (M) ({Base}_{M}) = Cntr (M)$
5	1 4	eqtr4i	$⊢ Z = Cntz (M) ({Base}_{M})$
6		ssid	$⊢ {Base}_{M} \subseteq {Base}_{M}$
7	2 3	cntzsubg	$⊢ (M \in Grp \land {Base}_{M} \subseteq {Base}_{M}) \to Cntz (M) ({Base}_{M}) \in SubGrp (M)$
8	6 7	mpan2	$⊢ M \in Grp \to Cntz (M) ({Base}_{M}) \in SubGrp (M)$
9	5 8	eqeltrid	$⊢ M \in Grp \to Z \in SubGrp (M)$
10		ssid	$⊢ Z \subseteq Z$
11	1	cntrsubgnsg	$⊢ (Z \in SubGrp (M) \land Z \subseteq Z) \to Z \in NrmSGrp (M)$
12	9 10 11	sylancl	$⊢ M \in Grp \to Z \in NrmSGrp (M)$

Metamath Proof Explorer