MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gex Structured version   Unicode version

Definition df-gex 16032
Description: Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.)
Assertion
Ref Expression
df-gex  |- gEx  =  ( g  e.  _V  |->  [_ { n  e.  NN  |  A. x  e.  (
Base `  g )
( n (.g `  g
) x )  =  ( 0g `  g
) }  /  i ]_ if ( i  =  (/) ,  0 ,  sup ( i ,  RR ,  `'  <  ) ) )
Distinct variable group:    g, i, n, x

Detailed syntax breakdown of Definition df-gex
StepHypRef Expression
1 cgex 16028 . 2  class gEx
2 vg . . 3  setvar  g
3 cvv 2971 . . 3  class  _V
4 vi . . . 4  setvar  i
5 vn . . . . . . . . 9  setvar  n
65cv 1368 . . . . . . . 8  class  n
7 vx . . . . . . . . 9  setvar  x
87cv 1368 . . . . . . . 8  class  x
92cv 1368 . . . . . . . . 9  class  g
10 cmg 15413 . . . . . . . . 9  class .g
119, 10cfv 5417 . . . . . . . 8  class  (.g `  g
)
126, 8, 11co 6090 . . . . . . 7  class  ( n (.g `  g ) x )
13 c0g 14377 . . . . . . . 8  class  0g
149, 13cfv 5417 . . . . . . 7  class  ( 0g
`  g )
1512, 14wceq 1369 . . . . . 6  wff  ( n (.g `  g ) x )  =  ( 0g
`  g )
16 cbs 14173 . . . . . . 7  class  Base
179, 16cfv 5417 . . . . . 6  class  ( Base `  g )
1815, 7, 17wral 2714 . . . . 5  wff  A. x  e.  ( Base `  g
) ( n (.g `  g ) x )  =  ( 0g `  g )
19 cn 10321 . . . . 5  class  NN
2018, 5, 19crab 2718 . . . 4  class  { n  e.  NN  |  A. x  e.  ( Base `  g
) ( n (.g `  g ) x )  =  ( 0g `  g ) }
214cv 1368 . . . . . 6  class  i
22 c0 3636 . . . . . 6  class  (/)
2321, 22wceq 1369 . . . . 5  wff  i  =  (/)
24 cc0 9281 . . . . 5  class  0
25 cr 9280 . . . . . 6  class  RR
26 clt 9417 . . . . . . 7  class  <
2726ccnv 4838 . . . . . 6  class  `'  <
2821, 25, 27csup 7689 . . . . 5  class  sup (
i ,  RR ,  `'  <  )
2923, 24, 28cif 3790 . . . 4  class  if ( i  =  (/) ,  0 ,  sup ( i ,  RR ,  `'  <  ) )
304, 20, 29csb 3287 . . 3  class  [_ {
n  e.  NN  |  A. x  e.  ( Base `  g ) ( n (.g `  g ) x )  =  ( 0g
`  g ) }  /  i ]_ if ( i  =  (/) ,  0 ,  sup (
i ,  RR ,  `'  <  ) )
312, 3, 30cmpt 4349 . 2  class  ( g  e.  _V  |->  [_ {
n  e.  NN  |  A. x  e.  ( Base `  g ) ( n (.g `  g ) x )  =  ( 0g
`  g ) }  /  i ]_ if ( i  =  (/) ,  0 ,  sup (
i ,  RR ,  `'  <  ) ) )
321, 31wceq 1369 1  wff gEx  =  ( g  e.  _V  |->  [_ { n  e.  NN  |  A. x  e.  (
Base `  g )
( n (.g `  g
) x )  =  ( 0g `  g
) }  /  i ]_ if ( i  =  (/) ,  0 ,  sup ( i ,  RR ,  `'  <  ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  gexval  16076
  Copyright terms: Public domain W3C validator