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

Theorem subgmulg 13318
Description: A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
Hypotheses
Ref Expression
subgmulgcl.t  |-  .x.  =  (.g
`  G )
subgmulg.h  |-  H  =  ( Gs  S )
subgmulg.t  |-  .xb  =  (.g
`  H )
Assertion
Ref Expression
subgmulg  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  ( N  .x.  X )  =  ( N  .xb  X
) )

Proof of Theorem subgmulg
StepHypRef Expression
1 subgmulg.h . . . . . 6  |-  H  =  ( Gs  S )
2 eqid 2196 . . . . . 6  |-  ( 0g
`  G )  =  ( 0g `  G
)
31, 2subg0 13310 . . . . 5  |-  ( S  e.  (SubGrp `  G
)  ->  ( 0g `  G )  =  ( 0g `  H ) )
433ad2ant1 1020 . . . 4  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  ( 0g `  G )  =  ( 0g `  H
) )
54ifeq1d 3578 . . 3  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  if ( N  =  0 ,  ( 0g `  G ) ,  if ( 0  <  N ,  (  seq 1
( ( +g  `  G
) ,  ( NN 
X.  { X }
) ) `  N
) ,  ( ( invg `  G
) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) )  =  if ( N  =  0 ,  ( 0g `  H
) ,  if ( 0  <  N , 
(  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) ) )
61a1i 9 . . . . . . . . . . 11  |-  ( S  e.  (SubGrp `  G
)  ->  H  =  ( Gs  S ) )
7 eqid 2196 . . . . . . . . . . . 12  |-  ( +g  `  G )  =  ( +g  `  G )
87a1i 9 . . . . . . . . . . 11  |-  ( S  e.  (SubGrp `  G
)  ->  ( +g  `  G )  =  ( +g  `  G ) )
9 id 19 . . . . . . . . . . 11  |-  ( S  e.  (SubGrp `  G
)  ->  S  e.  (SubGrp `  G ) )
10 subgrcl 13309 . . . . . . . . . . 11  |-  ( S  e.  (SubGrp `  G
)  ->  G  e.  Grp )
116, 8, 9, 10ressplusgd 12806 . . . . . . . . . 10  |-  ( S  e.  (SubGrp `  G
)  ->  ( +g  `  G )  =  ( +g  `  H ) )
12113ad2ant1 1020 . . . . . . . . 9  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  ( +g  `  G )  =  ( +g  `  H
) )
1312seqeq2d 10546 . . . . . . . 8  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) )  =  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) )
1413adantr 276 . . . . . . 7  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  -.  N  =  0 )  ->  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) )  =  seq 1 ( ( +g  `  H
) ,  ( NN 
X.  { X }
) ) )
1514fveq1d 5560 . . . . . 6  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  -.  N  =  0 )  ->  (  seq 1
( ( +g  `  G
) ,  ( NN 
X.  { X }
) ) `  N
)  =  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  N ) )
1615ifeq1d 3578 . . . . 5  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  -.  N  =  0 )  ->  if ( 0  <  N ,  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) )  =  if ( 0  <  N ,  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) )
17 simprl 529 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  ( -.  N  =  0  /\  -.  0  <  N
) )  ->  -.  N  =  0 )
18 simprr 531 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  ( -.  N  =  0  /\  -.  0  <  N
) )  ->  -.  0  <  N )
19 simp2 1000 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  N  e.  ZZ )
20 ztri3or0 9368 . . . . . . . . . . . 12  |-  ( N  e.  ZZ  ->  ( N  <  0  \/  N  =  0  \/  0  <  N ) )
2119, 20syl 14 . . . . . . . . . . 11  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  ( N  <  0  \/  N  =  0  \/  0  <  N ) )
2221adantr 276 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  ( -.  N  =  0  /\  -.  0  <  N
) )  ->  ( N  <  0  \/  N  =  0  \/  0  <  N ) )
2317, 18, 22ecase23d 1361 . . . . . . . . 9  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  ( -.  N  =  0  /\  -.  0  <  N
) )  ->  N  <  0 )
24 simpl1 1002 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  S  e.  (SubGrp `  G )
)
2519adantr 276 . . . . . . . . . . . . . 14  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  N  e.  ZZ )
2625znegcld 9450 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  -u N  e.  ZZ )
2719zred 9448 . . . . . . . . . . . . . . 15  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  N  e.  RR )
2827lt0neg1d 8542 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  ( N  <  0  <->  0  <  -u N ) )
2928biimpa 296 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  0  <  -u N )
30 elnnz 9336 . . . . . . . . . . . . 13  |-  ( -u N  e.  NN  <->  ( -u N  e.  ZZ  /\  0  <  -u N ) )
3126, 29, 30sylanbrc 417 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  -u N  e.  NN )
32 eqid 2196 . . . . . . . . . . . . . . . 16  |-  ( Base `  G )  =  (
Base `  G )
3332subgss 13304 . . . . . . . . . . . . . . 15  |-  ( S  e.  (SubGrp `  G
)  ->  S  C_  ( Base `  G ) )
34333ad2ant1 1020 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  S  C_  ( Base `  G
) )
35 simp3 1001 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  X  e.  S )
3634, 35sseldd 3184 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  X  e.  ( Base `  G
) )
3736adantr 276 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  X  e.  ( Base `  G
) )
38 subgmulgcl.t . . . . . . . . . . . . 13  |-  .x.  =  (.g
`  G )
39 eqid 2196 . . . . . . . . . . . . 13  |-  seq 1
( ( +g  `  G
) ,  ( NN 
X.  { X }
) )  =  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) )
4032, 7, 38, 39mulgnn 13256 . . . . . . . . . . . 12  |-  ( (
-u N  e.  NN  /\  X  e.  ( Base `  G ) )  -> 
( -u N  .x.  X
)  =  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) )
4131, 37, 40syl2anc 411 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  ( -u N  .x.  X )  =  (  seq 1
( ( +g  `  G
) ,  ( NN 
X.  { X }
) ) `  -u N
) )
4235adantr 276 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  X  e.  S )
4338subgmulgcl 13317 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubGrp `  G )  /\  -u N  e.  ZZ  /\  X  e.  S )  ->  ( -u N  .x.  X )  e.  S )
4424, 26, 42, 43syl3anc 1249 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  ( -u N  .x.  X )  e.  S )
4541, 44eqeltrrd 2274 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N )  e.  S
)
46 eqid 2196 . . . . . . . . . . 11  |-  ( invg `  G )  =  ( invg `  G )
47 eqid 2196 . . . . . . . . . . 11  |-  ( invg `  H )  =  ( invg `  H )
481, 46, 47subginv 13311 . . . . . . . . . 10  |-  ( ( S  e.  (SubGrp `  G )  /\  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N )  e.  S
)  ->  ( ( invg `  G ) `
 (  seq 1
( ( +g  `  G
) ,  ( NN 
X.  { X }
) ) `  -u N
) )  =  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) )
4924, 45, 48syl2anc 411 . . . . . . . . 9  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  N  <  0 )  ->  (
( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) )  =  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) )
5023, 49syldan 282 . . . . . . . 8  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  ( -.  N  =  0  /\  -.  0  <  N
) )  ->  (
( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) )  =  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) )
5113adantr 276 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  ( -.  N  =  0  /\  -.  0  <  N
) )  ->  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) )  =  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) )
5251fveq1d 5560 . . . . . . . . 9  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  ( -.  N  =  0  /\  -.  0  <  N
) )  ->  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N )  =  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `
 -u N ) )
5352fveq2d 5562 . . . . . . . 8  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  ( -.  N  =  0  /\  -.  0  <  N
) )  ->  (
( invg `  H ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) )  =  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  -u N ) ) )
5450, 53eqtrd 2229 . . . . . . 7  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  ( -.  N  =  0  /\  -.  0  <  N
) )  ->  (
( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) )  =  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  -u N ) ) )
5554anassrs 400 . . . . . 6  |-  ( ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  -.  N  =  0 )  /\  -.  0  <  N )  -> 
( ( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) )  =  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  -u N ) ) )
56 0z 9337 . . . . . . 7  |-  0  e.  ZZ
5719adantr 276 . . . . . . 7  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  -.  N  =  0 )  ->  N  e.  ZZ )
58 zdclt 9403 . . . . . . 7  |-  ( ( 0  e.  ZZ  /\  N  e.  ZZ )  -> DECID  0  <  N )
5956, 57, 58sylancr 414 . . . . . 6  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  -.  N  =  0 )  -> DECID  0  <  N )
6055, 59ifeq2dadc 3592 . . . . 5  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  -.  N  =  0 )  ->  if ( 0  <  N ,  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) )  =  if ( 0  <  N ,  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) )
6116, 60eqtrd 2229 . . . 4  |-  ( ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  /\  -.  N  =  0 )  ->  if ( 0  <  N ,  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) )  =  if ( 0  <  N ,  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) )
62 0zd 9338 . . . . 5  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  0  e.  ZZ )
63 zdceq 9401 . . . . 5  |-  ( ( N  e.  ZZ  /\  0  e.  ZZ )  -> DECID  N  =  0 )
6419, 62, 63syl2anc 411 . . . 4  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  -> DECID  N  =  0
)
6561, 64ifeq2dadc 3592 . . 3  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  if ( N  =  0 ,  ( 0g `  H ) ,  if ( 0  <  N ,  (  seq 1
( ( +g  `  G
) ,  ( NN 
X.  { X }
) ) `  N
) ,  ( ( invg `  G
) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) )  =  if ( N  =  0 ,  ( 0g `  H
) ,  if ( 0  <  N , 
(  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) ) )
665, 65eqtrd 2229 . 2  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  if ( N  =  0 ,  ( 0g `  G ) ,  if ( 0  <  N ,  (  seq 1
( ( +g  `  G
) ,  ( NN 
X.  { X }
) ) `  N
) ,  ( ( invg `  G
) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) )  =  if ( N  =  0 ,  ( 0g `  H
) ,  if ( 0  <  N , 
(  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) ) )
6732, 7, 2, 46, 38, 39mulgval 13252 . . 3  |-  ( ( N  e.  ZZ  /\  X  e.  ( Base `  G ) )  -> 
( N  .x.  X
)  =  if ( N  =  0 ,  ( 0g `  G
) ,  if ( 0  <  N , 
(  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) ) )
6819, 36, 67syl2anc 411 . 2  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  ( N  .x.  X )  =  if ( N  =  0 ,  ( 0g
`  G ) ,  if ( 0  < 
N ,  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  N ) ,  ( ( invg `  G ) `  (  seq 1 ( ( +g  `  G ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) ) )
691subgbas 13308 . . . . 5  |-  ( S  e.  (SubGrp `  G
)  ->  S  =  ( Base `  H )
)
70693ad2ant1 1020 . . . 4  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  S  =  ( Base `  H
) )
7135, 70eleqtrd 2275 . . 3  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  X  e.  ( Base `  H
) )
72 eqid 2196 . . . 4  |-  ( Base `  H )  =  (
Base `  H )
73 eqid 2196 . . . 4  |-  ( +g  `  H )  =  ( +g  `  H )
74 eqid 2196 . . . 4  |-  ( 0g
`  H )  =  ( 0g `  H
)
75 subgmulg.t . . . 4  |-  .xb  =  (.g
`  H )
76 eqid 2196 . . . 4  |-  seq 1
( ( +g  `  H
) ,  ( NN 
X.  { X }
) )  =  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) )
7772, 73, 74, 47, 75, 76mulgval 13252 . . 3  |-  ( ( N  e.  ZZ  /\  X  e.  ( Base `  H ) )  -> 
( N  .xb  X
)  =  if ( N  =  0 ,  ( 0g `  H
) ,  if ( 0  <  N , 
(  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `
 N ) ,  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) ) )
7819, 71, 77syl2anc 411 . 2  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  ( N  .xb  X )  =  if ( N  =  0 ,  ( 0g
`  H ) ,  if ( 0  < 
N ,  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  N ) ,  ( ( invg `  H ) `  (  seq 1 ( ( +g  `  H ) ,  ( NN  X.  { X } ) ) `  -u N ) ) ) ) )
7966, 68, 783eqtr4d 2239 1  |-  ( ( S  e.  (SubGrp `  G )  /\  N  e.  ZZ  /\  X  e.  S )  ->  ( N  .x.  X )  =  ( N  .xb  X
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104  DECID wdc 835    \/ w3o 979    /\ w3a 980    = wceq 1364    e. wcel 2167    C_ wss 3157   ifcif 3561   {csn 3622   class class class wbr 4033    X. cxp 4661   ` cfv 5258  (class class class)co 5922   0cc0 7879   1c1 7880    < clt 8061   -ucneg 8198   NNcn 8990   ZZcz 9326    seqcseq 10539   Basecbs 12678   ↾s cress 12679   +g cplusg 12755   0gc0g 12927   Grpcgrp 13132   invgcminusg 13133  .gcmg 13249  SubGrpcsubg 13297
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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-addcom 7979  ax-addass 7981  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-0id 7987  ax-rnegex 7988  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-ltadd 7995
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-if 3562  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-iord 4401  df-on 4403  df-ilim 4404  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-recs 6363  df-frec 6449  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-inn 8991  df-2 9049  df-n0 9250  df-z 9327  df-uz 9602  df-seqfrec 10540  df-ndx 12681  df-slot 12682  df-base 12684  df-sets 12685  df-iress 12686  df-plusg 12768  df-0g 12929  df-mgm 12999  df-sgrp 13045  df-mnd 13058  df-grp 13135  df-minusg 13136  df-mulg 13250  df-subg 13300
This theorem is referenced by:  zringmulg  14154
  Copyright terms: Public domain W3C validator