Theorem nsgsubg 19373

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 2760	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2760	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3	1, 2	isnsg 19370	. 2 ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ↔ (𝑦(+g‘𝐺)𝑥) ∈ 𝑆)))
4	3	simplbi 502	1 ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2144  ∀wral 3076  ‘cfv 6538  (class class class)co 7420  Basecbs 17392  +_gcplusg 17433  SubGrpcsubg 19335  NrmSGrpcnsg 19336

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7423  df-subg 19338  df-nsg 19339

This theorem is used by:  nsgconj  19374  isnsg3  19375  trivnsgd  19387  eqgcpbl  19399  qusgrp  19406  quseccl  19407  qusadd  19408  qus0  19409  qusinv  19410  qussub  19411  ecqusaddcl  19413  ghmnsgima  19459  ghmnsgpreima  19460  conjnsg  19473  qusghm  19474  ghmqusnsglem1  19499  ghmqusnsglem2  19500  ghmqusnsg  19501  ghmquskerlem1  19502  ghmquskerlem2  19504  ghmquskerlem3  19505  ghmqusker  19506  sylow3lem4  19849  prmgrpsimpgd  20335  rhmqusnsg  21586  rngqiprngimf1lem  21595  rngqiprngimf1  21601  rngqiprngimfo  21602  rngqiprngfulem4  21615  rngqipring1  21617  qsnzr  21644  clsnsg  24434  qustgpopn  24444  qustgphaus  24447  cyc3genpm  33759  qusker  33956  qus0g  34004  qusima  34005  qusrn  34006  nsgqus0  34007  nsgmgclem  34008  nsgmgc  34009  nsgqusf1olem1  34010  nsgqusf1olem2  34011  nsgqusf1olem3  34012  lmhmqusker  34014  rhmquskerlem  34021  opprqusplusg  34059  opprqus0g  34060  qsdrngilem  34064  qsdrngi  34065