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 ( 𝑖 , ℝ , < ) ) ) )