This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Detailed syntax breakdown

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