Metamath Proof Explorer

Theorem ssnmz

Description: A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-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 )
Assertion ssnmz 
|- ( S e. ( SubGrp ` G ) -> S C_ N )

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 2 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ X )
5 4 sselda 
 |-  ( ( S e. ( SubGrp ` G ) /\ z e. S ) -> z e. X )
6 simpll 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> S e. ( SubGrp ` G ) )
7 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
8 6 7 syl 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> G e. Grp )
9 6 4 syl 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> S C_ X )
10 simplrl 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> z e. S )
11 9 10 sseldd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> z e. X )
12 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
13 eqid 
 |-  ( invg ` G ) = ( invg ` G )
14 2 3 12 13 grplinv 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( ( invg ` G ) ` z ) .+ z ) = ( 0g ` G ) )
15 8 11 14 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( ( ( invg ` G ) ` z ) .+ z ) = ( 0g ` G ) )
16 15 oveq1d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( ( ( ( invg ` G ) ` z ) .+ z ) .+ w ) = ( ( 0g ` G ) .+ w ) )
17 13 subginvcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ z e. S ) -> ( ( invg ` G ) ` z ) e. S )
18 6 10 17 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( ( invg ` G ) ` z ) e. S )
19 9 18 sseldd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( ( invg ` G ) ` z ) e. X )
20 simplrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> w e. X )
21 2 3 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 8 19 11 20 21 syl13anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( ( ( ( invg ` G ) ` z ) .+ z ) .+ w ) = ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) )
23 2 3 12 grplid 
 |-  ( ( G e. Grp /\ w e. X ) -> ( ( 0g ` G ) .+ w ) = w )
24 8 20 23 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( ( 0g ` G ) .+ w ) = w )
25 16 22 24 3eqtr3d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) = w )
26 simpr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( z .+ w ) e. S )
27 3 subgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( ( invg ` G ) ` z ) e. S /\ ( z .+ w ) e. S ) -> ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) e. S )
28 6 18 26 27 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( ( ( invg ` G ) ` z ) .+ ( z .+ w ) ) e. S )
29 25 28 eqeltrrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> w e. S )
30 3 subgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ w e. S /\ z e. S ) -> ( w .+ z ) e. S )
31 6 29 10 30 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( z .+ w ) e. S ) -> ( w .+ z ) e. S )
32 simpll 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> S e. ( SubGrp ` G ) )
33 simplrl 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> z e. S )
34 32 7 syl 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> G e. Grp )
35 simplrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> w e. X )
36 32 33 5 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> z e. X )
37 eqid 
 |-  ( -g ` G ) = ( -g ` G )
38 2 3 37 grppncan 
 |-  ( ( G e. Grp /\ w e. X /\ z e. X ) -> ( ( w .+ z ) ( -g ` G ) z ) = w )
39 34 35 36 38 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> ( ( w .+ z ) ( -g ` G ) z ) = w )
40 simpr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> ( w .+ z ) e. S )
41 37 subgsubcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( w .+ z ) e. S /\ z e. S ) -> ( ( w .+ z ) ( -g ` G ) z ) e. S )
42 32 40 33 41 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> ( ( w .+ z ) ( -g ` G ) z ) e. S )
43 39 42 eqeltrrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> w e. S )
44 3 subgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ z e. S /\ w e. S ) -> ( z .+ w ) e. S )
45 32 33 43 44 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) /\ ( w .+ z ) e. S ) -> ( z .+ w ) e. S )
46 31 45 impbida 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( z e. S /\ w e. X ) ) -> ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) )
47 46 anassrs 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ z e. S ) /\ w e. X ) -> ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) )
48 47 ralrimiva 
 |-  ( ( S e. ( SubGrp ` G ) /\ z e. S ) -> A. w e. X ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) )
49 1 elnmz 
 |-  ( z e. N <-> ( z e. X /\ A. w e. X ( ( z .+ w ) e. S <-> ( w .+ z ) e. S ) ) )
50 5 48 49 sylanbrc 
 |-  ( ( S e. ( SubGrp ` G ) /\ z e. S ) -> z e. N )
51 50 ex 
 |-  ( S e. ( SubGrp ` G ) -> ( z e. S -> z e. N ) )
52 51 ssrdv 
 |-  ( S e. ( SubGrp ` G ) -> S C_ N )