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

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