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

Definition df-od 16047
Description: Define the order of an element in a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.)
Assertion
Ref Expression
df-od  |-  od  =  ( g  e.  _V  |->  ( x  e.  ( Base `  g )  |->  [_ { n  e.  NN  |  ( 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-od
StepHypRef Expression
1 cod 16043 . 2  class  od
2 vg . . 3  setvar  g
3 cvv 2987 . . 3  class  _V
4 vx . . . 4  setvar  x
52cv 1368 . . . . 5  class  g
6 cbs 14189 . . . . 5  class  Base
75, 6cfv 5433 . . . 4  class  ( Base `  g )
8 vi . . . . 5  setvar  i
9 vn . . . . . . . . 9  setvar  n
109cv 1368 . . . . . . . 8  class  n
114cv 1368 . . . . . . . 8  class  x
12 cmg 15429 . . . . . . . . 9  class .g
135, 12cfv 5433 . . . . . . . 8  class  (.g `  g
)
1410, 11, 13co 6106 . . . . . . 7  class  ( n (.g `  g ) x )
15 c0g 14393 . . . . . . . 8  class  0g
165, 15cfv 5433 . . . . . . 7  class  ( 0g
`  g )
1714, 16wceq 1369 . . . . . 6  wff  ( n (.g `  g ) x )  =  ( 0g
`  g )
18 cn 10337 . . . . . 6  class  NN
1917, 9, 18crab 2734 . . . . 5  class  { n  e.  NN  |  ( n (.g `  g ) x )  =  ( 0g
`  g ) }
208cv 1368 . . . . . . 7  class  i
21 c0 3652 . . . . . . 7  class  (/)
2220, 21wceq 1369 . . . . . 6  wff  i  =  (/)
23 cc0 9297 . . . . . 6  class  0
24 cr 9296 . . . . . . 7  class  RR
25 clt 9433 . . . . . . . 8  class  <
2625ccnv 4854 . . . . . . 7  class  `'  <
2720, 24, 26csup 7705 . . . . . 6  class  sup (
i ,  RR ,  `'  <  )
2822, 23, 27cif 3806 . . . . 5  class  if ( i  =  (/) ,  0 ,  sup ( i ,  RR ,  `'  <  ) )
298, 19, 28csb 3303 . . . 4  class  [_ {
n  e.  NN  | 
( n (.g `  g
) x )  =  ( 0g `  g
) }  /  i ]_ if ( i  =  (/) ,  0 ,  sup ( i ,  RR ,  `'  <  ) )
304, 7, 29cmpt 4365 . . 3  class  ( x  e.  ( Base `  g
)  |->  [_ { n  e.  NN  |  ( n (.g `  g ) x )  =  ( 0g
`  g ) }  /  i ]_ if ( i  =  (/) ,  0 ,  sup (
i ,  RR ,  `'  <  ) ) )
312, 3, 30cmpt 4365 . 2  class  ( g  e.  _V  |->  ( x  e.  ( Base `  g
)  |->  [_ { n  e.  NN  |  ( n (.g `  g ) x )  =  ( 0g
`  g ) }  /  i ]_ if ( i  =  (/) ,  0 ,  sup (
i ,  RR ,  `'  <  ) ) ) )
321, 31wceq 1369 1  wff  od  =  ( g  e.  _V  |->  ( x  e.  ( Base `  g )  |->  [_ { n  e.  NN  |  ( n (.g `  g ) x )  =  ( 0g `  g ) }  / 
i ]_ if ( i  =  (/) ,  0 ,  sup ( i ,  RR ,  `'  <  ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  odfval  16051
  Copyright terms: Public domain W3C validator