MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gex Structured version   Visualization version   GIF version

Definition df-gex 18588
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.)
Assertion
Ref Expression
df-gex gEx = (𝑔 ∈ V ↦ {𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g𝑔)𝑥) = (0g𝑔)} / 𝑖if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
Distinct variable group:   𝑔,𝑖,𝑛,𝑥

Detailed syntax breakdown of Definition df-gex
StepHypRef Expression
1 cgex 18584 . 2 class gEx
2 vg . . 3 setvar 𝑔
3 cvv 3495 . . 3 class V
4 vi . . . 4 setvar 𝑖
5 vn . . . . . . . . 9 setvar 𝑛
65cv 1527 . . . . . . . 8 class 𝑛
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1527 . . . . . . . 8 class 𝑥
92cv 1527 . . . . . . . . 9 class 𝑔
10 cmg 18164 . . . . . . . . 9 class .g
119, 10cfv 6349 . . . . . . . 8 class (.g𝑔)
126, 8, 11co 7145 . . . . . . 7 class (𝑛(.g𝑔)𝑥)
13 c0g 16703 . . . . . . . 8 class 0g
149, 13cfv 6349 . . . . . . 7 class (0g𝑔)
1512, 14wceq 1528 . . . . . 6 wff (𝑛(.g𝑔)𝑥) = (0g𝑔)
16 cbs 16473 . . . . . . 7 class Base
179, 16cfv 6349 . . . . . 6 class (Base‘𝑔)
1815, 7, 17wral 3138 . . . . 5 wff 𝑥 ∈ (Base‘𝑔)(𝑛(.g𝑔)𝑥) = (0g𝑔)
19 cn 11627 . . . . 5 class
2018, 5, 19crab 3142 . . . 4 class {𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g𝑔)𝑥) = (0g𝑔)}
214cv 1527 . . . . . 6 class 𝑖
22 c0 4290 . . . . . 6 class
2321, 22wceq 1528 . . . . 5 wff 𝑖 = ∅
24 cc0 10526 . . . . 5 class 0
25 cr 10525 . . . . . 6 class
26 clt 10664 . . . . . 6 class <
2721, 25, 26cinf 8894 . . . . 5 class inf(𝑖, ℝ, < )
2823, 24, 27cif 4465 . . . 4 class if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
294, 20, 28csb 3882 . . 3 class {𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g𝑔)𝑥) = (0g𝑔)} / 𝑖if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
302, 3, 29cmpt 5138 . 2 class (𝑔 ∈ V ↦ {𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g𝑔)𝑥) = (0g𝑔)} / 𝑖if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
311, 30wceq 1528 1 wff gEx = (𝑔 ∈ V ↦ {𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g𝑔)𝑥) = (0g𝑔)} / 𝑖if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
Colors of variables: wff setvar class
This definition is referenced by:  gexval  18634
  Copyright terms: Public domain W3C validator