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 = Base G
gexval.2 ⊢ · ˙ = ⋅ G
gexval.3 ⊢ 0 ˙ = 0 G
gexval.4 ⊢ E = gEx ⁡ G
gexval.i ⊢ I = y ∈ ℕ | ∀ x ∈ X y · ˙ x = 0 ˙
Assertion gexval ⊢ G ∈ V → E = if I = ∅ 0 inf I ℝ <

Proof

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