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