Metamath Proof Explorer

Theorem nmznsg

Description: Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses elnmz.1 
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }
nmzsubg.2 
|- X = ( Base ` G )
nmzsubg.3 
|- .+ = ( +g ` G )
nmznsg.4 
|- H = ( G |`s N )
Assertion nmznsg 
|- ( S e. ( SubGrp ` G ) -> S e. ( NrmSGrp ` H ) )

Proof

Step Hyp Ref Expression
1 elnmz.1 
 |-  N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }
2 nmzsubg.2 
 |-  X = ( Base ` G )
3 nmzsubg.3 
 |-  .+ = ( +g ` G )
4 nmznsg.4 
 |-  H = ( G |`s N )
5 id 
 |-  ( S e. ( SubGrp ` G ) -> S e. ( SubGrp ` G ) )
6 1 2 3 ssnmz 
 |-  ( S e. ( SubGrp ` G ) -> S C_ N )
7 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
8 1 2 3 nmzsubg 
 |-  ( G e. Grp -> N e. ( SubGrp ` G ) )
9 7 8 syl 
 |-  ( S e. ( SubGrp ` G ) -> N e. ( SubGrp ` G ) )
10 4 subsubg 
 |-  ( N e. ( SubGrp ` G ) -> ( S e. ( SubGrp ` H ) <-> ( S e. ( SubGrp ` G ) /\ S C_ N ) ) )
11 9 10 syl 
 |-  ( S e. ( SubGrp ` G ) -> ( S e. ( SubGrp ` H ) <-> ( S e. ( SubGrp ` G ) /\ S C_ N ) ) )
12 5 6 11 mpbir2and 
 |-  ( S e. ( SubGrp ` G ) -> S e. ( SubGrp ` H ) )
13 1 ssrab3 
 |-  N C_ X
14 13 sseli 
 |-  ( w e. N -> w e. X )
15 1 nmzbi 
 |-  ( ( z e. N /\ w e. X ) -> ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) )
16 14 15 sylan2 
 |-  ( ( z e. N /\ w e. N ) -> ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) )
17 16 rgen2 
 |-  A. z e. N A. w e. N ( ( z .+ w ) e. S <-> ( w .+ z ) e. S )
18 4 subgbas 
 |-  ( N e. ( SubGrp ` G ) -> N = ( Base ` H ) )
19 9 18 syl 
 |-  ( S e. ( SubGrp ` G ) -> N = ( Base ` H ) )
20 19 raleqdv 
 |-  ( S e. ( SubGrp ` G ) -> ( A. w e. N ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) <-> A. w e. ( Base ` H ) ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) ) )
21 19 20 raleqbidv 
 |-  ( S e. ( SubGrp ` G ) -> ( A. z e. N A. w e. N ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) <-> A. z e. ( Base ` H ) A. w e. ( Base ` H ) ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) ) )
22 17 21 mpbii 
 |-  ( S e. ( SubGrp ` G ) -> A. z e. ( Base ` H ) A. w e. ( Base ` H ) ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) )
23 eqid 
 |-  ( Base ` H ) = ( Base ` H )
24 2 fvexi 
 |-  X e. _V
25 24 13 ssexi 
 |-  N e. _V
26 4 3 ressplusg 
 |-  ( N e. _V -> .+ = ( +g ` H ) )
27 25 26 ax-mp 
 |-  .+ = ( +g ` H )
28 23 27 isnsg 
 |-  ( S e. ( NrmSGrp ` H ) <-> ( S e. ( SubGrp ` H ) /\ A. z e. ( Base ` H ) A. w e. ( Base ` H ) ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) ) )
29 12 22 28 sylanbrc 
 |-  ( S e. ( SubGrp ` G ) -> S e. ( NrmSGrp ` H ) )