Theorem isnsg 19138

Description: Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)

Hypotheses

Ref	Expression
isnsg.1	⊢ 𝑋 = (Base‘𝐺)
isnsg.2	⊢ + = (+g‘𝐺)

Assertion

Ref	Expression
isnsg	⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))

Distinct variable groups:   𝑥,𝑦,𝐺   𝑥, + ,𝑦   𝑥,𝑆,𝑦   𝑥,𝑋,𝑦

Proof of Theorem isnsg

Dummy variables 𝑔 𝑏 𝑝 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-nsg 19107	. . 3 ⊢ NrmSGrp = (𝑔 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑔) ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})
2	1	mptrcl 6995	. 2 ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐺 ∈ Grp)
3		subgrcl 19114	. . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
4	3	adantr 480	. 2 ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)) → 𝐺 ∈ Grp)
5		fveq2 6876	. . . . . 6 ⊢ (𝑔 = 𝐺 → (SubGrp‘𝑔) = (SubGrp‘𝐺))
6		fvexd 6891	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) ∈ V)
7		fveq2 6876	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺))
8		isnsg.1	. . . . . . . 8 ⊢ 𝑋 = (Base‘𝐺)
9	7, 8	eqtr4di 2788	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑋)
10		fvexd 6891	. . . . . . . 8 ⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) ∈ V)
11		simpl 482	. . . . . . . . . 10 ⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → 𝑔 = 𝐺)
12	11	fveq2d 6880	. . . . . . . . 9 ⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) = (+g‘𝐺))
13		isnsg.2	. . . . . . . . 9 ⊢ + = (+g‘𝐺)
14	12, 13	eqtr4di 2788	. . . . . . . 8 ⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) = + )
15		simplr 768	. . . . . . . . 9 ⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → 𝑏 = 𝑋)
16		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → 𝑝 = + )
17	16	oveqd 7422	. . . . . . . . . . . 12 ⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦))
18	17	eleq1d 2819	. . . . . . . . . . 11 ⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑥 + 𝑦) ∈ 𝑠))
19	16	oveqd 7422	. . . . . . . . . . . 12 ⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (𝑦𝑝𝑥) = (𝑦 + 𝑥))
20	19	eleq1d 2819	. . . . . . . . . . 11 ⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → ((𝑦𝑝𝑥) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))
21	18, 20	bibi12d 345	. . . . . . . . . 10 ⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)))
22	15, 21	raleqbidv 3325	. . . . . . . . 9 ⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)))
23	15, 22	raleqbidv 3325	. . . . . . . 8 ⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)))
24	10, 14, 23	sbcied2 3810	. . . . . . 7 ⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → ([(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)))
25	6, 9, 24	sbcied2 3810	. . . . . 6 ⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)))
26	5, 25	rabeqbidv 3434	. . . . 5 ⊢ (𝑔 = 𝐺 → {𝑠 ∈ (SubGrp‘𝑔) ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)} = {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)})
27		fvex 6889	. . . . . 6 ⊢ (SubGrp‘𝐺) ∈ V
28	27	rabex 5309	. . . . 5 ⊢ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} ∈ V
29	26, 1, 28	fvmpt 6986	. . . 4 ⊢ (𝐺 ∈ Grp → (NrmSGrp‘𝐺) = {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)})
30	29	eleq2d 2820	. . 3 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (NrmSGrp‘𝐺) ↔ 𝑆 ∈ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)}))
31		eleq2 2823	. . . . . 6 ⊢ (𝑠 = 𝑆 → ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑥 + 𝑦) ∈ 𝑆))
32		eleq2 2823	. . . . . 6 ⊢ (𝑠 = 𝑆 → ((𝑦 + 𝑥) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑆))
33	31, 32	bibi12d 345	. . . . 5 ⊢ (𝑠 = 𝑆 → (((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠) ↔ ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))
34	33	2ralbidv 3205	. . . 4 ⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))
35	34	elrab 3671	. . 3 ⊢ (𝑆 ∈ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))
36	30, 35	bitrdi 287	. 2 ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))))
37	2, 4, 36	pm5.21nii 378	1 ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3051  {crab 3415  Vcvv 3459  [wsbc 3765  ‘cfv 6531  (class class class)co 7405  Basecbs 17228  +_gcplusg 17271  Grpcgrp 18916  SubGrpcsubg 19103  NrmSGrpcnsg 19104

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fv 6539  df-ov 7408  df-subg 19106  df-nsg 19107

This theorem is referenced by:  isnsg2  19139  nsgbi  19140  nsgsubg  19141  isnsg4  19150  nmznsg  19151  ablnsg  19828  rzgrp  21583