Theorem isnsg3

Description: A subgroup is normal iff the conjugation of all the elements of the subgroup is in the subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	isnsg3.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	isnsg3.2	⊢ + = ( +g ‘ 𝐺 )
	isnsg3.3	⊢ − = ( -g ‘ 𝐺 )
Assertion	isnsg3	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		isnsg3.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		isnsg3.2	⊢ + = ( +g ‘ 𝐺 )
3		isnsg3.3	⊢ − = ( -g ‘ 𝐺 )
4		nsgsubg	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
5	1 2 3	nsgconj	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 )
6	5	3expb	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 )
7	6	ralrimivva	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 )
8	4 7	jca	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) )
9		simpl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
10		subgrcl	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
11	10	ad2antrr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → 𝐺 ∈ Grp )
12		simprll	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → 𝑧 ∈ 𝑋 )
13		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
14		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
15	1 2 13 14	grplinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) = ( 0g ‘ 𝐺 ) )
16	11 12 15	syl2anc	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) = ( 0g ‘ 𝐺 ) )
17	16	oveq1d	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) + 𝑤 ) = ( ( 0g ‘ 𝐺 ) + 𝑤 ) )
18	1 14	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
19	11 12 18	syl2anc	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 )
20		simprlr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → 𝑤 ∈ 𝑋 )
21	1 2	grpass	⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) + 𝑤 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) )
22	11 19 12 20 21	syl13anc	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑧 ) + 𝑤 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) )
23	1 2 13	grplid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑤 ) = 𝑤 )
24	11 20 23	syl2anc	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( ( 0g ‘ 𝐺 ) + 𝑤 ) = 𝑤 )
25	17 22 24	3eqtr3d	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) = 𝑤 )
26	25	oveq1d	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) = ( 𝑤 − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
27	1 2 3 14 11 20 12	grpsubinv	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( 𝑤 − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) = ( 𝑤 + 𝑧 ) )
28	26 27	eqtrd	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) = ( 𝑤 + 𝑧 ) )
29		simprr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( 𝑧 + 𝑤 ) ∈ 𝑆 )
30		simplr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 )
31		oveq1	⊢ ( 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) → ( 𝑥 + 𝑦 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑦 ) )
32		id	⊢ ( 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) → 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) )
33	31 32	oveq12d	⊢ ( 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) → ( ( 𝑥 + 𝑦 ) − 𝑥 ) = ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑦 ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
34	33	eleq1d	⊢ ( 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) → ( ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑦 ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
35		oveq2	⊢ ( 𝑦 = ( 𝑧 + 𝑤 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑦 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) )
36	35	oveq1d	⊢ ( 𝑦 = ( 𝑧 + 𝑤 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑦 ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) = ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) )
37	36	eleq1d	⊢ ( 𝑦 = ( 𝑧 + 𝑤 ) → ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + 𝑦 ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 ) )
38	34 37	rspc2va	⊢ ( ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ∈ 𝑋 ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 )
39	19 29 30 38	syl21anc	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) + ( 𝑧 + 𝑤 ) ) − ( ( invg ‘ 𝐺 ) ‘ 𝑧 ) ) ∈ 𝑆 )
40	28 39	eqeltrrd	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 + 𝑤 ) ∈ 𝑆 ) ) → ( 𝑤 + 𝑧 ) ∈ 𝑆 )
41	40	expr	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑧 + 𝑤 ) ∈ 𝑆 → ( 𝑤 + 𝑧 ) ∈ 𝑆 ) )
42	41	ralrimivva	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 → ( 𝑤 + 𝑧 ) ∈ 𝑆 ) )
43	1 2	isnsg2	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 → ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) )
44	9 42 43	sylanbrc	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) → 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) )
45	8 44	impbii	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 + 𝑦 ) − 𝑥 ) ∈ 𝑆 ) )