Theorem nsgsubg

Description: A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Assertion	nsgsubg	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to S\in \mathrm{SubGrp}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
2		eqid	$$⊢{+}_G={+}_G$$
3	1 2	isnsg	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in {\mathrm{Base}}_G\forall y\in {\mathrm{Base}}_G\left(x{+}_{G}y\in S\leftrightarrow y{+}_{G}x\in S\right)\right)$$
4	3	simplbi	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to S\in \mathrm{SubGrp}\left(G\right)$$