cntrsubgnsg

Description: A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015)

		Ref	Expression
	Hypothesis	cntrnsg.z	$⊢ Z = Cntr (M)$
	Assertion	cntrsubgnsg	$⊢ (X \in SubGrp (M) \land X \subseteq Z) \to X \in NrmSGrp (M)$

Proof

Step	Hyp	Ref	Expression
1		cntrnsg.z	$⊢ Z = Cntr (M)$
2		simpl	$⊢ (X \in SubGrp (M) \land X \subseteq Z) \to X \in SubGrp (M)$
3		simplr	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to X \subseteq Z$
4		simprr	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to y \in X$
5	3 4	sseldd	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to y \in Z$
6		eqid	$⊢ {Base}_{M} = {Base}_{M}$
7		eqid	$⊢ Cntz (M) = Cntz (M)$
8	6 7	cntrval	$⊢ Cntz (M) ({Base}_{M}) = Cntr (M)$
9	8 1	eqtr4i	$⊢ Cntz (M) ({Base}_{M}) = Z$
10	5 9	eleqtrrdi	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to y \in Cntz (M) ({Base}_{M})$
11		simprl	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to x \in {Base}_{M}$
12		eqid	$⊢ +_{M} = +_{M}$
13	12 7	cntzi	$⊢ (y \in Cntz (M) ({Base}_{M}) \land x \in {Base}_{M}) \to y +_{M} x = x +_{M} y$
14	10 11 13	syl2anc	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to y +_{M} x = x +_{M} y$
15	14	oveq1d	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to (y +_{M} x) -_{M} x = (x +_{M} y) -_{M} x$
16		subgrcl	$⊢ X \in SubGrp (M) \to M \in Grp$
17	16	ad2antrr	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to M \in Grp$
18	6	subgss	$⊢ X \in SubGrp (M) \to X \subseteq {Base}_{M}$
19	18	ad2antrr	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to X \subseteq {Base}_{M}$
20	19 4	sseldd	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to y \in {Base}_{M}$
21		eqid	$⊢ -_{M} = -_{M}$
22	6 12 21	grppncan	$⊢ (M \in Grp \land y \in {Base}_{M} \land x \in {Base}_{M}) \to (y +_{M} x) -_{M} x = y$
23	17 20 11 22	syl3anc	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to (y +_{M} x) -_{M} x = y$
24	15 23	eqtr3d	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to (x +_{M} y) -_{M} x = y$
25	24 4	eqeltrd	$⊢ ((X \in SubGrp (M) \land X \subseteq Z) \land (x \in {Base}_{M} \land y \in X)) \to (x +_{M} y) -_{M} x \in X$
26	25	ralrimivva	$⊢ (X \in SubGrp (M) \land X \subseteq Z) \to \forall x \in {Base}_{M} \forall y \in X (x +_{M} y) -_{M} x \in X$
27	6 12 21	isnsg3	$⊢ X \in NrmSGrp (M) \leftrightarrow (X \in SubGrp (M) \land \forall x \in {Base}_{M} \forall y \in X (x +_{M} y) -_{M} x \in X)$
28	2 26 27	sylanbrc	$⊢ (X \in SubGrp (M) \land X \subseteq Z) \to X \in NrmSGrp (M)$

Metamath Proof Explorer

Theorem cntrsubgnsg

Proof