Metamath Proof Explorer

Theorem cyggex2

Description: The exponent of a cyclic group is 0 if the group is infinite, otherwise it equals the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses cygctb.1 ⊢ B = Base G
cyggex.o ⊢ E = gEx ⁡ G
Assertion cyggex2 ⊢ G ∈ CycGrp → E = if B ∈ Fin B 0

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢ B = Base G
2 cyggex.o ⊢ E = gEx ⁡ G
3 eqid ⊢ ⋅ G = ⋅ G
4 eqid ⊢ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
5 1 3 4 iscyg2 ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ≠ ∅
6 n0 ⊢ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ≠ ∅ ↔ ∃ y y ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
7 ssrab2 ⊢ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ⊆ B
8 simpr ⊢ G ∈ Grp ∧ y ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → y ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
9 7 8 sselid ⊢ G ∈ Grp ∧ y ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → y ∈ B
10 eqid ⊢ od ⁡ G = od ⁡ G
11 1 3 4 10 cyggenod2 ⊢ G ∈ Grp ∧ y ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → od ⁡ G ⁡ y = if B ∈ Fin B 0
12 9 11 jca ⊢ G ∈ Grp ∧ y ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0
13 12 ex ⊢ G ∈ Grp → y ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0
14 1 2 gexcl ⊢ G ∈ Grp → E ∈ ℕ 0
15 14 adantr ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 → E ∈ ℕ 0
16 hashcl ⊢ B ∈ Fin → B ∈ ℕ 0
17 16 adantl ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 ∧ B ∈ Fin → B ∈ ℕ 0
18 0nn0 ⊢ 0 ∈ ℕ 0
19 18 a1i ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 ∧ ¬ B ∈ Fin → 0 ∈ ℕ 0
20 17 19 ifclda ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 → if B ∈ Fin B 0 ∈ ℕ 0
21 breq2 ⊢ B = if B ∈ Fin B 0 → E ∥ B ↔ E ∥ if B ∈ Fin B 0
22 breq2 ⊢ 0 = if B ∈ Fin B 0 → E ∥ 0 ↔ E ∥ if B ∈ Fin B 0
23 1 2 gexdvds3 ⊢ G ∈ Grp ∧ B ∈ Fin → E ∥ B
24 23 adantlr ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 ∧ B ∈ Fin → E ∥ B
25 15 adantr ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 ∧ ¬ B ∈ Fin → E ∈ ℕ 0
26 nn0z ⊢ E ∈ ℕ 0 → E ∈ ℤ
27 dvds0 ⊢ E ∈ ℤ → E ∥ 0
28 25 26 27 3syl ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 ∧ ¬ B ∈ Fin → E ∥ 0
29 21 22 24 28 ifbothda ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 → E ∥ if B ∈ Fin B 0
30 simprr ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 → od ⁡ G ⁡ y = if B ∈ Fin B 0
31 1 2 10 gexod ⊢ G ∈ Grp ∧ y ∈ B → od ⁡ G ⁡ y ∥ E
32 31 adantrr ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 → od ⁡ G ⁡ y ∥ E
33 30 32 eqbrtrrd ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 → if B ∈ Fin B 0 ∥ E
34 dvdseq ⊢ E ∈ ℕ 0 ∧ if B ∈ Fin B 0 ∈ ℕ 0 ∧ E ∥ if B ∈ Fin B 0 ∧ if B ∈ Fin B 0 ∥ E → E = if B ∈ Fin B 0
35 15 20 29 33 34 syl22anc ⊢ G ∈ Grp ∧ y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 → E = if B ∈ Fin B 0
36 35 ex ⊢ G ∈ Grp → y ∈ B ∧ od ⁡ G ⁡ y = if B ∈ Fin B 0 → E = if B ∈ Fin B 0
37 13 36 syld ⊢ G ∈ Grp → y ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → E = if B ∈ Fin B 0
38 37 exlimdv ⊢ G ∈ Grp → ∃ y y ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → E = if B ∈ Fin B 0
39 6 38 biimtrid ⊢ G ∈ Grp → x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ≠ ∅ → E = if B ∈ Fin B 0
40 39 imp ⊢ G ∈ Grp ∧ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ≠ ∅ → E = if B ∈ Fin B 0
41 5 40 sylbi ⊢ G ∈ CycGrp → E = if B ∈ Fin B 0