Metamath Proof Explorer

Definition df-od

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) (Revised by AV, 5-Oct-2020)

Ref Expression
Assertion df-od 
|- od = ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cod 
 |-  od
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( Base ` g )
7 vn 
 |-  n
8 cn 
 |-  NN
9 7 cv 
 |-  n
10 cmg 
 |-  .g
11 5 10 cfv 
 |-  ( .g ` g )
12 3 cv 
 |-  x
13 9 12 11 co 
 |-  ( n ( .g ` g ) x )
14 c0g 
 |-  0g
15 5 14 cfv 
 |-  ( 0g ` g )
16 13 15 wceq 
 |-  ( n ( .g ` g ) x ) = ( 0g ` g )
17 16 7 8 crab 
 |-  { n e. NN | ( n ( .g ` g ) x ) = ( 0g ` g ) }
18 vi 
 |-  i
19 18 cv 
 |-  i
20 c0 
 |-  (/)
21 19 20 wceq 
 |-  i = (/)
22 cc0 
 |-  0
23 cr 
 |-  RR
24 clt 
 |-  <
25 19 23 24 cinf 
 |-  inf ( i , RR , < )
26 21 22 25 cif 
 |-  if ( i = (/) , 0 , inf ( i , RR , < ) )
27 18 17 26 csb 
 |-  [_ { n e. NN | ( n ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) )
28 3 6 27 cmpt 
 |-  ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
29 1 2 28 cmpt 
 |-  ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )
30 0 29 wceq 
 |-  od = ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { n e. NN | ( n ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )