Theorem nsgsubg 19113

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2099  ∀wral 3058  ‘cfv 6548  (class class class)co 7420  Basecbs 17180  +_gcplusg 17233  SubGrpcsubg 19075  NrmSGrpcnsg 19076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fv 6556  df-ov 7423  df-subg 19078  df-nsg 19079

This theorem is referenced by:  nsgconj  19114  isnsg3  19115  trivnsgd  19127  eqgcpbl  19137  qusgrp  19141  quseccl  19142  qusadd  19143  qus0  19144  qusinv  19145  qussub  19146  ecqusaddcl  19148  ghmnsgima  19194  ghmnsgpreima  19195  conjnsg  19208  qusghm  19209  ghmquskerlem1  19234  ghmquskerlem2  19236  ghmquskerlem3  19237  ghmqusker  19238  sylow3lem4  19585  prmgrpsimpgd  20071  rngqiprngimf1lem  21184  rngqiprngimf1  21190  rngqiprngimfo  21191  rngqiprngfulem4  21204  rngqipring1  21206  clsnsg  24027  qustgpopn  24037  qustgphaus  24040  cyc3genpm  32886  qusker  33074  qus0g  33130  qusima  33131  qusrn  33132  nsgqus0  33133  nsgmgclem  33134  nsgmgc  33135  nsgqusf1olem1  33136  nsgqusf1olem2  33137  nsgqusf1olem3  33138  lmhmqusker  33140  ghmqusnsglem1  33142  ghmqusnsglem2  33143  ghmqusnsg  33144  rhmquskerlem  33153  rhmqusnsg  33156  qsnzr  33184  opprqusplusg  33213  opprqus0g  33214  qsdrngilem  33218  qsdrngi  33219