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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
cyggex.o ⊢ 𝐸 = ( gEx ‘ 𝐺 )
Assertion cyggex2 ( 𝐺 ∈ CycGrp → 𝐸 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 cyggex.o ⊢ 𝐸 = ( gEx ‘ 𝐺 )
3 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
4 eqid ⊢ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 }
5 1 3 4 iscyg2 ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ≠ ∅ ) )
6 n0 ⊢ ( { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } )
7 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ⊆ 𝐵
8 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } )
9 7 8 sseldi ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ) → 𝑦 ∈ 𝐵 )
10 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
11 1 3 4 10 cyggenod2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
12 9 11 jca ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ) → ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) )
13 12 ex ⊢ ( 𝐺 ∈ Grp → ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } → ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) )
14 1 2 gexcl ⊢ ( 𝐺 ∈ Grp → 𝐸 ∈ ℕ0 )
15 14 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) → 𝐸 ∈ ℕ0 )
16 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
17 16 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
18 0nn0 ⊢ 0 ∈ ℕ0
19 18 a1i ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) ∧ ¬ 𝐵 ∈ Fin ) → 0 ∈ ℕ0 )
20 17 19 ifclda ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ∈ ℕ0 )
21 breq2 ⊢ ( ( ♯ ‘ 𝐵 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) → ( 𝐸 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝐸 ∥ if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) )
22 breq2 ⊢ ( 0 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) → ( 𝐸 ∥ 0 ↔ 𝐸 ∥ if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) )
23 1 2 gexdvds3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ) → 𝐸 ∥ ( ♯ ‘ 𝐵 ) )
24 23 adantlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) ∧ 𝐵 ∈ Fin ) → 𝐸 ∥ ( ♯ ‘ 𝐵 ) )
25 15 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) ∧ ¬ 𝐵 ∈ Fin ) → 𝐸 ∈ ℕ0 )
26 nn0z ⊢ ( 𝐸 ∈ ℕ0 → 𝐸 ∈ ℤ )
27 dvds0 ⊢ ( 𝐸 ∈ ℤ → 𝐸 ∥ 0 )
28 25 26 27 3syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) ∧ ¬ 𝐵 ∈ Fin ) → 𝐸 ∥ 0 )
29 21 22 24 28 ifbothda ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) → 𝐸 ∥ if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
30 simprr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
31 1 2 10 gexod ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝐸 )
32 31 adantrr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝐸 )
33 30 32 eqbrtrrd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ∥ 𝐸 )
34 dvdseq ⊢ ( ( ( 𝐸 ∈ ℕ0 ∧ if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ∈ ℕ0 ) ∧ ( 𝐸 ∥ if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ∧ if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ∥ 𝐸 ) ) → 𝐸 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
35 15 20 29 33 34 syl22anc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) ) → 𝐸 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
36 35 ex ⊢ ( 𝐺 ∈ Grp → ( ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) → 𝐸 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) )
37 13 36 syld ⊢ ( 𝐺 ∈ Grp → ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } → 𝐸 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) )
38 37 exlimdv ⊢ ( 𝐺 ∈ Grp → ( ∃ 𝑦 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } → 𝐸 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) )
39 6 38 syl5bi ⊢ ( 𝐺 ∈ Grp → ( { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ≠ ∅ → 𝐸 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ) )
40 39 imp ⊢ ( ( 𝐺 ∈ Grp ∧ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 } ≠ ∅ ) → 𝐸 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
41 5 40 sylbi ⊢ ( 𝐺 ∈ CycGrp → 𝐸 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )