ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nmzsubg Unicode version

Theorem nmzsubg 13280
Description: The normalizer NG(S) of a subset  S of the group is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
Hypotheses
Ref Expression
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
Ref Expression
nmzsubg  |-  ( G  e.  Grp  ->  N  e.  (SubGrp `  G )
)
Distinct variable groups:    x, y, G   
x, S, y    x,  .+ , y    x, X, y
Allowed substitution hints:    N( x, y)

Proof of Theorem nmzsubg
Dummy variables  z  w  u  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elnmz.1 . . . 4  |-  N  =  { x  e.  X  |  A. y  e.  X  ( ( x  .+  y )  e.  S  <->  ( y  .+  x )  e.  S ) }
21ssrab3 3265 . . 3  |-  N  C_  X
32a1i 9 . 2  |-  ( G  e.  Grp  ->  N  C_  X )
4 nmzsubg.2 . . . . 5  |-  X  =  ( Base `  G
)
5 eqid 2193 . . . . 5  |-  ( 0g
`  G )  =  ( 0g `  G
)
64, 5grpidcl 13101 . . . 4  |-  ( G  e.  Grp  ->  ( 0g `  G )  e.  X )
7 nmzsubg.3 . . . . . . . 8  |-  .+  =  ( +g  `  G )
84, 7, 5grplid 13103 . . . . . . 7  |-  ( ( G  e.  Grp  /\  z  e.  X )  ->  ( ( 0g `  G )  .+  z
)  =  z )
94, 7, 5grprid 13104 . . . . . . 7  |-  ( ( G  e.  Grp  /\  z  e.  X )  ->  ( z  .+  ( 0g `  G ) )  =  z )
108, 9eqtr4d 2229 . . . . . 6  |-  ( ( G  e.  Grp  /\  z  e.  X )  ->  ( ( 0g `  G )  .+  z
)  =  ( z 
.+  ( 0g `  G ) ) )
1110eleq1d 2262 . . . . 5  |-  ( ( G  e.  Grp  /\  z  e.  X )  ->  ( ( ( 0g
`  G )  .+  z )  e.  S  <->  ( z  .+  ( 0g
`  G ) )  e.  S ) )
1211ralrimiva 2567 . . . 4  |-  ( G  e.  Grp  ->  A. z  e.  X  ( (
( 0g `  G
)  .+  z )  e.  S  <->  ( z  .+  ( 0g `  G ) )  e.  S ) )
131elnmz 13278 . . . 4  |-  ( ( 0g `  G )  e.  N  <->  ( ( 0g `  G )  e.  X  /\  A. z  e.  X  ( (
( 0g `  G
)  .+  z )  e.  S  <->  ( z  .+  ( 0g `  G ) )  e.  S ) ) )
146, 12, 13sylanbrc 417 . . 3  |-  ( G  e.  Grp  ->  ( 0g `  G )  e.  N )
15 elex2 2776 . . 3  |-  ( ( 0g `  G )  e.  N  ->  E. a 
a  e.  N )
1614, 15syl 14 . 2  |-  ( G  e.  Grp  ->  E. a 
a  e.  N )
17 id 19 . . . . . . . 8  |-  ( G  e.  Grp  ->  G  e.  Grp )
182sseli 3175 . . . . . . . 8  |-  ( z  e.  N  ->  z  e.  X )
192sseli 3175 . . . . . . . 8  |-  ( w  e.  N  ->  w  e.  X )
204, 7grpcl 13080 . . . . . . . 8  |-  ( ( G  e.  Grp  /\  z  e.  X  /\  w  e.  X )  ->  ( z  .+  w
)  e.  X )
2117, 18, 19, 20syl3an 1291 . . . . . . 7  |-  ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  ->  ( z  .+  w
)  e.  X )
22 simpl1 1002 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  G  e.  Grp )
23 simpl2 1003 . . . . . . . . . . . 12  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  z  e.  N )
242, 23sselid 3177 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  z  e.  X )
25 simpl3 1004 . . . . . . . . . . . 12  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  w  e.  N )
262, 25sselid 3177 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  w  e.  X )
27 simpr 110 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  u  e.  X )
284, 7grpass 13081 . . . . . . . . . . 11  |-  ( ( G  e.  Grp  /\  ( z  e.  X  /\  w  e.  X  /\  u  e.  X
) )  ->  (
( z  .+  w
)  .+  u )  =  ( z  .+  ( w  .+  u ) ) )
2922, 24, 26, 27, 28syl13anc 1251 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
z  .+  w )  .+  u )  =  ( z  .+  ( w 
.+  u ) ) )
3029eleq1d 2262 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
( z  .+  w
)  .+  u )  e.  S  <->  ( z  .+  ( w  .+  u ) )  e.  S ) )
314, 7, 22, 26, 27grpcld 13086 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( w  .+  u )  e.  X
)
321nmzbi 13279 . . . . . . . . . . 11  |-  ( ( z  e.  N  /\  ( w  .+  u )  e.  X )  -> 
( ( z  .+  ( w  .+  u ) )  e.  S  <->  ( (
w  .+  u )  .+  z )  e.  S
) )
3323, 31, 32syl2anc 411 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
z  .+  ( w  .+  u ) )  e.  S  <->  ( ( w 
.+  u )  .+  z )  e.  S
) )
344, 7grpass 13081 . . . . . . . . . . . 12  |-  ( ( G  e.  Grp  /\  ( w  e.  X  /\  u  e.  X  /\  z  e.  X
) )  ->  (
( w  .+  u
)  .+  z )  =  ( w  .+  ( u  .+  z ) ) )
3522, 26, 27, 24, 34syl13anc 1251 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
w  .+  u )  .+  z )  =  ( w  .+  ( u 
.+  z ) ) )
3635eleq1d 2262 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
( w  .+  u
)  .+  z )  e.  S  <->  ( w  .+  ( u  .+  z ) )  e.  S ) )
374, 7, 22, 27, 24grpcld 13086 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( u  .+  z )  e.  X
)
381nmzbi 13279 . . . . . . . . . . 11  |-  ( ( w  e.  N  /\  ( u  .+  z )  e.  X )  -> 
( ( w  .+  ( u  .+  z ) )  e.  S  <->  ( (
u  .+  z )  .+  w )  e.  S
) )
3925, 37, 38syl2anc 411 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
w  .+  ( u  .+  z ) )  e.  S  <->  ( ( u 
.+  z )  .+  w )  e.  S
) )
4033, 36, 393bitrd 214 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
z  .+  ( w  .+  u ) )  e.  S  <->  ( ( u 
.+  z )  .+  w )  e.  S
) )
414, 7grpass 13081 . . . . . . . . . . 11  |-  ( ( G  e.  Grp  /\  ( u  e.  X  /\  z  e.  X  /\  w  e.  X
) )  ->  (
( u  .+  z
)  .+  w )  =  ( u  .+  ( z  .+  w
) ) )
4222, 27, 24, 26, 41syl13anc 1251 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
u  .+  z )  .+  w )  =  ( u  .+  ( z 
.+  w ) ) )
4342eleq1d 2262 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
( u  .+  z
)  .+  w )  e.  S  <->  ( u  .+  ( z  .+  w
) )  e.  S
) )
4430, 40, 433bitrd 214 . . . . . . . 8  |-  ( ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  /\  u  e.  X
)  ->  ( (
( z  .+  w
)  .+  u )  e.  S  <->  ( u  .+  ( z  .+  w
) )  e.  S
) )
4544ralrimiva 2567 . . . . . . 7  |-  ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  ->  A. u  e.  X  ( ( ( z 
.+  w )  .+  u )  e.  S  <->  ( u  .+  ( z 
.+  w ) )  e.  S ) )
461elnmz 13278 . . . . . . 7  |-  ( ( z  .+  w )  e.  N  <->  ( (
z  .+  w )  e.  X  /\  A. u  e.  X  ( (
( z  .+  w
)  .+  u )  e.  S  <->  ( u  .+  ( z  .+  w
) )  e.  S
) ) )
4721, 45, 46sylanbrc 417 . . . . . 6  |-  ( ( G  e.  Grp  /\  z  e.  N  /\  w  e.  N )  ->  ( z  .+  w
)  e.  N )
48473expa 1205 . . . . 5  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  w  e.  N
)  ->  ( z  .+  w )  e.  N
)
4948ralrimiva 2567 . . . 4  |-  ( ( G  e.  Grp  /\  z  e.  N )  ->  A. w  e.  N  ( z  .+  w
)  e.  N )
50 eqid 2193 . . . . . . 7  |-  ( invg `  G )  =  ( invg `  G )
514, 50grpinvcl 13120 . . . . . 6  |-  ( ( G  e.  Grp  /\  z  e.  X )  ->  ( ( invg `  G ) `  z
)  e.  X )
5218, 51sylan2 286 . . . . 5  |-  ( ( G  e.  Grp  /\  z  e.  N )  ->  ( ( invg `  G ) `  z
)  e.  X )
53 simplr 528 . . . . . . . 8  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  z  e.  N )
54 simpll 527 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  G  e.  Grp )
5552adantr 276 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( ( invg `  G ) `
 z )  e.  X )
56 simpr 110 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  u  e.  X )
574, 7, 54, 56, 55grpcld 13086 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( u  .+  ( ( invg `  G ) `  z
) )  e.  X
)
584, 7, 54, 55, 57grpcld 13086 . . . . . . . 8  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) )  e.  X )
591nmzbi 13279 . . . . . . . 8  |-  ( ( z  e.  N  /\  ( ( ( invg `  G ) `
 z )  .+  ( u  .+  ( ( invg `  G
) `  z )
) )  e.  X
)  ->  ( (
z  .+  ( (
( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) ) )  e.  S  <->  ( (
( ( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) )  .+  z )  e.  S
) )
6053, 58, 59syl2anc 411 . . . . . . 7  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
z  .+  ( (
( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) ) )  e.  S  <->  ( (
( ( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) )  .+  z )  e.  S
) )
612, 53sselid 3177 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  z  e.  X )
624, 7, 5, 50grprinv 13123 . . . . . . . . . . 11  |-  ( ( G  e.  Grp  /\  z  e.  X )  ->  ( z  .+  (
( invg `  G ) `  z
) )  =  ( 0g `  G ) )
6354, 61, 62syl2anc 411 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( z  .+  ( ( invg `  G ) `  z
) )  =  ( 0g `  G ) )
6463oveq1d 5933 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
z  .+  ( ( invg `  G ) `
 z ) ) 
.+  ( u  .+  ( ( invg `  G ) `  z
) ) )  =  ( ( 0g `  G )  .+  (
u  .+  ( ( invg `  G ) `
 z ) ) ) )
654, 7grpass 13081 . . . . . . . . . 10  |-  ( ( G  e.  Grp  /\  ( z  e.  X  /\  ( ( invg `  G ) `  z
)  e.  X  /\  ( u  .+  ( ( invg `  G
) `  z )
)  e.  X ) )  ->  ( (
z  .+  ( ( invg `  G ) `
 z ) ) 
.+  ( u  .+  ( ( invg `  G ) `  z
) ) )  =  ( z  .+  (
( ( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) ) ) )
6654, 61, 55, 57, 65syl13anc 1251 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
z  .+  ( ( invg `  G ) `
 z ) ) 
.+  ( u  .+  ( ( invg `  G ) `  z
) ) )  =  ( z  .+  (
( ( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) ) ) )
674, 7, 5grplid 13103 . . . . . . . . . 10  |-  ( ( G  e.  Grp  /\  ( u  .+  ( ( invg `  G
) `  z )
)  e.  X )  ->  ( ( 0g
`  G )  .+  ( u  .+  ( ( invg `  G
) `  z )
) )  =  ( u  .+  ( ( invg `  G
) `  z )
) )
6854, 57, 67syl2anc 411 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( ( 0g `  G )  .+  ( u  .+  ( ( invg `  G
) `  z )
) )  =  ( u  .+  ( ( invg `  G
) `  z )
) )
6964, 66, 683eqtr3d 2234 . . . . . . . 8  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( z  .+  ( ( ( invg `  G ) `
 z )  .+  ( u  .+  ( ( invg `  G
) `  z )
) ) )  =  ( u  .+  (
( invg `  G ) `  z
) ) )
7069eleq1d 2262 . . . . . . 7  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
z  .+  ( (
( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) ) )  e.  S  <->  ( u  .+  ( ( invg `  G ) `  z
) )  e.  S
) )
714, 7grpass 13081 . . . . . . . . . 10  |-  ( ( G  e.  Grp  /\  ( ( ( invg `  G ) `
 z )  e.  X  /\  ( u 
.+  ( ( invg `  G ) `
 z ) )  e.  X  /\  z  e.  X ) )  -> 
( ( ( ( invg `  G
) `  z )  .+  ( u  .+  (
( invg `  G ) `  z
) ) )  .+  z )  =  ( ( ( invg `  G ) `  z
)  .+  ( (
u  .+  ( ( invg `  G ) `
 z ) ) 
.+  z ) ) )
7254, 55, 57, 61, 71syl13anc 1251 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
( ( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) )  .+  z )  =  ( ( ( invg `  G ) `  z
)  .+  ( (
u  .+  ( ( invg `  G ) `
 z ) ) 
.+  z ) ) )
734, 7grpass 13081 . . . . . . . . . . . 12  |-  ( ( G  e.  Grp  /\  ( u  e.  X  /\  ( ( invg `  G ) `  z
)  e.  X  /\  z  e.  X )
)  ->  ( (
u  .+  ( ( invg `  G ) `
 z ) ) 
.+  z )  =  ( u  .+  (
( ( invg `  G ) `  z
)  .+  z )
) )
7454, 56, 55, 61, 73syl13anc 1251 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
u  .+  ( ( invg `  G ) `
 z ) ) 
.+  z )  =  ( u  .+  (
( ( invg `  G ) `  z
)  .+  z )
) )
754, 7, 5, 50grplinv 13122 . . . . . . . . . . . . 13  |-  ( ( G  e.  Grp  /\  z  e.  X )  ->  ( ( ( invg `  G ) `
 z )  .+  z )  =  ( 0g `  G ) )
7654, 61, 75syl2anc 411 . . . . . . . . . . . 12  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
( invg `  G ) `  z
)  .+  z )  =  ( 0g `  G ) )
7776oveq2d 5934 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( u  .+  ( ( ( invg `  G ) `
 z )  .+  z ) )  =  ( u  .+  ( 0g `  G ) ) )
784, 7, 5grprid 13104 . . . . . . . . . . . 12  |-  ( ( G  e.  Grp  /\  u  e.  X )  ->  ( u  .+  ( 0g `  G ) )  =  u )
7954, 56, 78syl2anc 411 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( u  .+  ( 0g `  G
) )  =  u )
8074, 77, 793eqtrd 2230 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
u  .+  ( ( invg `  G ) `
 z ) ) 
.+  z )  =  u )
8180oveq2d 5934 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
( invg `  G ) `  z
)  .+  ( (
u  .+  ( ( invg `  G ) `
 z ) ) 
.+  z ) )  =  ( ( ( invg `  G
) `  z )  .+  u ) )
8272, 81eqtrd 2226 . . . . . . . 8  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
( ( invg `  G ) `  z
)  .+  ( u  .+  ( ( invg `  G ) `  z
) ) )  .+  z )  =  ( ( ( invg `  G ) `  z
)  .+  u )
)
8382eleq1d 2262 . . . . . . 7  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
( ( ( invg `  G ) `
 z )  .+  ( u  .+  ( ( invg `  G
) `  z )
) )  .+  z
)  e.  S  <->  ( (
( invg `  G ) `  z
)  .+  u )  e.  S ) )
8460, 70, 833bitr3rd 219 . . . . . 6  |-  ( ( ( G  e.  Grp  /\  z  e.  N )  /\  u  e.  X
)  ->  ( (
( ( invg `  G ) `  z
)  .+  u )  e.  S  <->  ( u  .+  ( ( invg `  G ) `  z
) )  e.  S
) )
8584ralrimiva 2567 . . . . 5  |-  ( ( G  e.  Grp  /\  z  e.  N )  ->  A. u  e.  X  ( ( ( ( invg `  G
) `  z )  .+  u )  e.  S  <->  ( u  .+  ( ( invg `  G
) `  z )
)  e.  S ) )
861elnmz 13278 . . . . 5  |-  ( ( ( invg `  G ) `  z
)  e.  N  <->  ( (
( invg `  G ) `  z
)  e.  X  /\  A. u  e.  X  ( ( ( ( invg `  G ) `
 z )  .+  u )  e.  S  <->  ( u  .+  ( ( invg `  G
) `  z )
)  e.  S ) ) )
8752, 85, 86sylanbrc 417 . . . 4  |-  ( ( G  e.  Grp  /\  z  e.  N )  ->  ( ( invg `  G ) `  z
)  e.  N )
8849, 87jca 306 . . 3  |-  ( ( G  e.  Grp  /\  z  e.  N )  ->  ( A. w  e.  N  ( z  .+  w )  e.  N  /\  ( ( invg `  G ) `  z
)  e.  N ) )
8988ralrimiva 2567 . 2  |-  ( G  e.  Grp  ->  A. z  e.  N  ( A. w  e.  N  (
z  .+  w )  e.  N  /\  (
( invg `  G ) `  z
)  e.  N ) )
904, 7, 50issubg2m 13259 . 2  |-  ( G  e.  Grp  ->  ( N  e.  (SubGrp `  G
)  <->  ( N  C_  X  /\  E. a  a  e.  N  /\  A. z  e.  N  ( A. w  e.  N  ( z  .+  w
)  e.  N  /\  ( ( invg `  G ) `  z
)  e.  N ) ) ) )
913, 16, 89, 90mpbir3and 1182 1  |-  ( G  e.  Grp  ->  N  e.  (SubGrp `  G )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    /\ w3a 980    = wceq 1364   E.wex 1503    e. wcel 2164   A.wral 2472   {crab 2476    C_ wss 3153   ` cfv 5254  (class class class)co 5918   Basecbs 12618   +g cplusg 12695   0gc0g 12867   Grpcgrp 13072   invgcminusg 13073  SubGrpcsubg 13237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-addcom 7972  ax-addass 7974  ax-i2m1 7977  ax-0lt1 7978  ax-0id 7980  ax-rnegex 7981  ax-pre-ltirr 7984  ax-pre-ltadd 7988
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-pnf 8056  df-mnf 8057  df-ltxr 8059  df-inn 8983  df-2 9041  df-ndx 12621  df-slot 12622  df-base 12624  df-sets 12625  df-iress 12626  df-plusg 12708  df-0g 12869  df-mgm 12939  df-sgrp 12985  df-mnd 12998  df-grp 13075  df-minusg 13076  df-subg 13240
This theorem is referenced by:  nmznsg  13283
  Copyright terms: Public domain W3C validator