Theorem nsgsubg 19037

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

Assertion

Ref	Expression
nsgsubg	⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺))

Proof of Theorem nsgsubg

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2729	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3	1, 2	isnsg 19034	. 2 ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ↔ (𝑦(+g‘𝐺)𝑥) ∈ 𝑆)))
4	3	simplbi 497	1 ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∀wral 3044  ‘cfv 6482  (class class class)co 7349  Basecbs 17120  +_gcplusg 17161  SubGrpcsubg 18999  NrmSGrpcnsg 19000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fv 6490  df-ov 7352  df-subg 19002  df-nsg 19003

This theorem is referenced by:  nsgconj  19038  isnsg3  19039  trivnsgd  19051  eqgcpbl  19061  qusgrp  19065  quseccl  19066  qusadd  19067  qus0  19068  qusinv  19069  qussub  19070  ecqusaddcl  19072  ghmnsgima  19119  ghmnsgpreima  19120  conjnsg  19133  qusghm  19134  ghmqusnsglem1  19159  ghmqusnsglem2  19160  ghmqusnsg  19161  ghmquskerlem1  19162  ghmquskerlem2  19164  ghmquskerlem3  19165  ghmqusker  19166  sylow3lem4  19509  prmgrpsimpgd  19995  rhmqusnsg  21192  rngqiprngimf1lem  21201  rngqiprngimf1  21207  rngqiprngimfo  21208  rngqiprngfulem4  21221  rngqipring1  21223  clsnsg  23995  qustgpopn  24005  qustgphaus  24008  cyc3genpm  33095  qusker  33287  qus0g  33345  qusima  33346  qusrn  33347  nsgqus0  33348  nsgmgclem  33349  nsgmgc  33350  nsgqusf1olem1  33351  nsgqusf1olem2  33352  nsgqusf1olem3  33353  lmhmqusker  33355  rhmquskerlem  33363  qsnzr  33393  opprqusplusg  33427  opprqus0g  33428  qsdrngilem  33432  qsdrngi  33433