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 ∈ V ⟼ ⦋ n ∈ ℕ | ∀ x ∈ Base g n ⋅ g x = 0 g / i⦌ if i = ∅ 0 inf i ℝ <

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgex class gEx
1 vg setvar g
2 cvv class V
3 vn setvar n
4 cn class ℕ
5 vx setvar x
6 cbs class Base
7 1 cv setvar g
8 7 6 cfv class Base g
9 3 cv setvar n
10 cmg class ⋅ 𝑔
11 7 10 cfv class ⋅ g
12 5 cv setvar x
13 9 12 11 co class n ⋅ g x
14 c0g class 0 𝑔
15 7 14 cfv class 0 g
16 13 15 wceq wff n ⋅ g x = 0 g
17 16 5 8 wral wff ∀ x ∈ Base g n ⋅ g x = 0 g
18 17 3 4 crab class n ∈ ℕ | ∀ x ∈ Base g n ⋅ g x = 0 g
19 vi setvar i
20 19 cv setvar i
21 c0 class ∅
22 20 21 wceq wff i = ∅
23 cc0 class 0
24 cr class ℝ
25 clt class <
26 20 24 25 cinf class inf i ℝ <
27 22 23 26 cif class if i = ∅ 0 inf i ℝ <
28 19 18 27 csb class ⦋ n ∈ ℕ | ∀ x ∈ Base g n ⋅ g x = 0 g / i⦌ if i = ∅ 0 inf i ℝ <
29 1 2 28 cmpt class g ∈ V ⟼ ⦋ n ∈ ℕ | ∀ x ∈ Base g n ⋅ g x = 0 g / i⦌ if i = ∅ 0 inf i ℝ <
30 0 29 wceq wff gEx = g ∈ V ⟼ ⦋ n ∈ ℕ | ∀ x ∈ Base g n ⋅ g x = 0 g / i⦌ if i = ∅ 0 inf i ℝ <