Metamath Proof Explorer


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 ‘ 𝐺 ) ∧ ∀ 𝑥𝑋𝑦𝑆 ( ( 𝑥 + 𝑦 ) 𝑥 ) ∈ 𝑆 ) )