Metamath Proof Explorer

Theorem gexval

Description: Value of the exponent of a group. (Contributed by Mario Carneiro, 23-Apr-2016) (Revised by AV, 26-Sep-2020)

Ref Expression
Hypotheses gexval.1 ⊢X=BaseG
gexval.2 ⊢·˙=⋅G
gexval.3 ⊢0˙=0G
gexval.4 ⊢E=gEx⁡G
gexval.i ⊢I=y∈ℕ|∀x∈Xy·˙x=0˙
Assertion gexval ⊢G∈V→E=ifI=∅0supIℝ<

Proof

Step Hyp Ref Expression
1 gexval.1 ⊢X=BaseG
2 gexval.2 ⊢·˙=⋅G
3 gexval.3 ⊢0˙=0G
4 gexval.4 ⊢E=gEx⁡G
5 gexval.i ⊢I=y∈ℕ|∀x∈Xy·˙x=0˙
6 df-gex ⊢gEx=g∈V⟼⦋y∈ℕ|∀x∈Basegy⋅gx=0g/i⦌ifi=∅0supiℝ<
7 nnex ⊢ℕ∈V
8 7 rabex ⊢y∈ℕ|∀x∈Basegy⋅gx=0g∈V
9 8 a1i ⊢G∈V∧g=G→y∈ℕ|∀x∈Basegy⋅gx=0g∈V
10 simpr ⊢G∈V∧g=G→g=G
11 10 fveq2d ⊢G∈V∧g=G→Baseg=BaseG
12 11 1 eqtr4di ⊢G∈V∧g=G→Baseg=X
13 10 fveq2d ⊢G∈V∧g=G→⋅g=⋅G
14 13 2 eqtr4di ⊢G∈V∧g=G→⋅g=·˙
15 14 oveqd ⊢G∈V∧g=G→y⋅gx=y·˙x
16 10 fveq2d ⊢G∈V∧g=G→0g=0G
17 16 3 eqtr4di ⊢G∈V∧g=G→0g=0˙
18 15 17 eqeq12d ⊢G∈V∧g=G→y⋅gx=0g↔y·˙x=0˙
19 12 18 raleqbidv ⊢G∈V∧g=G→∀x∈Basegy⋅gx=0g↔∀x∈Xy·˙x=0˙
20 19 rabbidv ⊢G∈V∧g=G→y∈ℕ|∀x∈Basegy⋅gx=0g=y∈ℕ|∀x∈Xy·˙x=0˙
21 20 5 eqtr4di ⊢G∈V∧g=G→y∈ℕ|∀x∈Basegy⋅gx=0g=I
22 21 eqeq2d ⊢G∈V∧g=G→i=y∈ℕ|∀x∈Basegy⋅gx=0g↔i=I
23 22 biimpa ⊢G∈V∧g=G∧i=y∈ℕ|∀x∈Basegy⋅gx=0g→i=I
24 23 eqeq1d ⊢G∈V∧g=G∧i=y∈ℕ|∀x∈Basegy⋅gx=0g→i=∅↔I=∅
25 23 infeq1d ⊢G∈V∧g=G∧i=y∈ℕ|∀x∈Basegy⋅gx=0g→supiℝ<=supIℝ<
26 24 25 ifbieq2d ⊢G∈V∧g=G∧i=y∈ℕ|∀x∈Basegy⋅gx=0g→ifi=∅0supiℝ<=ifI=∅0supIℝ<
27 9 26 csbied ⊢G∈V∧g=G→⦋y∈ℕ|∀x∈Basegy⋅gx=0g/i⦌ifi=∅0supiℝ<=ifI=∅0supIℝ<
28 elex ⊢G∈V→G∈V
29 c0ex ⊢0∈V
30 ltso ⊢<Orℝ
31 30 infex ⊢supIℝ<∈V
32 29 31 ifex ⊢ifI=∅0supIℝ<∈V
33 32 a1i ⊢G∈V→ifI=∅0supIℝ<∈V
34 6 27 28 33 fvmptd2 ⊢G∈V→gEx⁡G=ifI=∅0supIℝ<
35 4 34 eqtrid ⊢G∈V→E=ifI=∅0supIℝ<