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 = ( 𝑔 ∈ V ↦ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g𝑔 ) 𝑥 ) = ( 0g𝑔 ) } / 𝑖 if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgex gEx
1 vg 𝑔
2 cvv V
3 vn 𝑛
4 cn
5 vx 𝑥
6 cbs Base
7 1 cv 𝑔
8 7 6 cfv ( Base ‘ 𝑔 )
9 3 cv 𝑛
10 cmg .g
11 7 10 cfv ( .g𝑔 )
12 5 cv 𝑥
13 9 12 11 co ( 𝑛 ( .g𝑔 ) 𝑥 )
14 c0g 0g
15 7 14 cfv ( 0g𝑔 )
16 13 15 wceq ( 𝑛 ( .g𝑔 ) 𝑥 ) = ( 0g𝑔 )
17 16 5 8 wral 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g𝑔 ) 𝑥 ) = ( 0g𝑔 )
18 17 3 4 crab { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g𝑔 ) 𝑥 ) = ( 0g𝑔 ) }
19 vi 𝑖
20 19 cv 𝑖
21 c0
22 20 21 wceq 𝑖 = ∅
23 cc0 0
24 cr
25 clt <
26 20 24 25 cinf inf ( 𝑖 , ℝ , < )
27 22 23 26 cif if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) )
28 19 18 27 csb { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g𝑔 ) 𝑥 ) = ( 0g𝑔 ) } / 𝑖 if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) )
29 1 2 28 cmpt ( 𝑔 ∈ V ↦ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g𝑔 ) 𝑥 ) = ( 0g𝑔 ) } / 𝑖 if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )
30 0 29 wceq gEx = ( 𝑔 ∈ V ↦ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g𝑔 ) 𝑥 ) = ( 0g𝑔 ) } / 𝑖 if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )