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 
|- X = ( Base ` G )
isnsg3.2 
|- .+ = ( +g ` G )
isnsg3.3 
|- .- = ( -g ` G )
Assertion isnsg3 
|- ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) )

Proof

Step Hyp Ref Expression
1 isnsg3.1 
 |-  X = ( Base ` G )
2 isnsg3.2 
 |-  .+ = ( +g ` G )
3 isnsg3.3 
 |-  .- = ( -g ` G )
4 nsgsubg 
 |-  ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )
5 1 2 3 nsgconj 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ x e. X /\ y e. S ) -> ( ( x .+ y ) .- x ) e. S )
6 5 3expb 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ ( x e. X /\ y e. S ) ) -> ( ( x .+ y ) .- x ) e. S )
7 6 ralrimivva 
 |-  ( S e. ( NrmSGrp ` G ) -> A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S )
8 4 7 jca 
 |-  ( S e. ( NrmSGrp ` G ) -> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) )
9 simpl 
 |-  ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) -> S e. ( SubGrp ` G ) )
10 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
11 10 ad2antrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> G e. Grp )
12 simprll 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> z e. X )
13 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
14 eqid 
 |-  ( invg ` G ) = ( invg ` G )
15 1 2 13 14 grplinv 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( ( invg ` G ) ` z ) .+ z ) = ( 0g ` G ) )
16 11 12 15 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( ( ( invg ` G ) ` z ) .+ z ) = ( 0g ` G ) )
17 16 oveq1d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( ( ( ( invg ` G ) ` z ) .+ z ) .+ w ) = ( ( 0g ` G ) .+ w ) )
18 1 14 grpinvcl 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( invg ` G ) ` z ) e. X )
19 11 12 18 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( ( invg ` G ) ` z ) e. X )
20 simprlr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> w e. X )
21 1 2 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` z ) e. X /\ z e. X /\ w e. X ) ) -> ( ( ( ( invg ` G ) ` z ) .+ z ) .+ w ) = ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) )
22 11 19 12 20 21 syl13anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( ( ( ( invg ` G ) ` z ) .+ z ) .+ w ) = ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) )
23 1 2 13 grplid 
 |-  ( ( G e. Grp /\ w e. X ) -> ( ( 0g ` G ) .+ w ) = w )
24 11 20 23 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( ( 0g ` G ) .+ w ) = w )
25 17 22 24 3eqtr3d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) = w )
26 25 oveq1d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) .- ( ( invg ` G ) ` z ) ) = ( w .- ( ( invg ` G ) ` z ) ) )
27 1 2 3 14 11 20 12 grpsubinv 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( w .- ( ( invg ` G ) ` z ) ) = ( w .+ z ) )
28 26 27 eqtrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) .- ( ( invg ` G ) ` z ) ) = ( w .+ z ) )
29 simprr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( z .+ w ) e. S )
30 simplr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S )
31 oveq1 
 |-  ( x = ( ( invg ` G ) ` z ) -> ( x .+ y ) = ( ( ( invg ` G ) ` z ) .+ y ) )
32 id 
 |-  ( x = ( ( invg ` G ) ` z ) -> x = ( ( invg ` G ) ` z ) )
33 31 32 oveq12d 
 |-  ( x = ( ( invg ` G ) ` z ) -> ( ( x .+ y ) .- x ) = ( ( ( ( invg ` G ) ` z ) .+ y ) .- ( ( invg ` G ) ` z ) ) )
34 33 eleq1d 
 |-  ( x = ( ( invg ` G ) ` z ) -> ( ( ( x .+ y ) .- x ) e. S <-> ( ( ( ( invg ` G ) ` z ) .+ y ) .- ( ( invg ` G ) ` z ) ) e. S ) )
35 oveq2 
 |-  ( y = ( z .+ w ) -> ( ( ( invg ` G ) ` z ) .+ y ) = ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) )
36 35 oveq1d 
 |-  ( y = ( z .+ w ) -> ( ( ( ( invg ` G ) ` z ) .+ y ) .- ( ( invg ` G ) ` z ) ) = ( ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) .- ( ( invg ` G ) ` z ) ) )
37 36 eleq1d 
 |-  ( y = ( z .+ w ) -> ( ( ( ( ( invg ` G ) ` z ) .+ y ) .- ( ( invg ` G ) ` z ) ) e. S <-> ( ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) .- ( ( invg ` G ) ` z ) ) e. S ) )
38 34 37 rspc2va 
 |-  ( ( ( ( ( invg ` G ) ` z ) e. X /\ ( z .+ w ) e. S ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) -> ( ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) .- ( ( invg ` G ) ` z ) ) e. S )
39 19 29 30 38 syl21anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) .- ( ( invg ` G ) ` z ) ) e. S )
40 28 39 eqeltrrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( ( z e. X /\ w e. X ) /\ ( z .+ w ) e. S ) ) -> ( w .+ z ) e. S )
41 40 expr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) /\ ( z e. X /\ w e. X ) ) -> ( ( z .+ w ) e. S -> ( w .+ z ) e. S ) )
42 41 ralrimivva 
 |-  ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) -> A. z e. X A. w e. X ( ( z .+ w ) e. S -> ( w .+ z ) e. S ) )
43 1 2 isnsg2 
 |-  ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. z e. X A. w e. X ( ( z .+ w ) e. S -> ( w .+ z ) e. S ) ) )
44 9 42 43 sylanbrc 
 |-  ( ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) -> S e. ( NrmSGrp ` G ) )
45 8 44 impbii 
 |-  ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. X A. y e. S ( ( x .+ y ) .- x ) e. S ) )