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

Detailed syntax breakdown

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