Metamath Proof Explorer


Definition df-gex

Description: Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by Stefan O'Rear, 4-Sep-2015) (Revised by AV, 26-Sep-2020)

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

Detailed syntax breakdown

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