Metamath Proof Explorer

Theorem dfod2

Description: An alternative definition of the order of a group element is as the cardinality of the cyclic subgroup generated by the element. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses odf1.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odf1.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odf1.3 ⊢ · = ( .g ‘ 𝐺 )
odf1.4 ⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
Assertion dfod2 ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = if ( ran 𝐹 ∈ Fin , ( ♯ ‘ ran 𝐹 ) , 0 ) )

Proof

Step Hyp Ref Expression
1 odf1.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odf1.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odf1.3 ⊢ · = ( .g ‘ 𝐺 )
4 odf1.4 ⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
5 fzfid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ∈ Fin )
6 1 3 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 )
7 6 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 )
8 7 an32s ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 )
9 8 adantlr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 )
10 9 4 fmptd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐹 : ℤ ⟶ 𝑋 )
11 frn ⊢ ( 𝐹 : ℤ ⟶ 𝑋 → ran 𝐹 ⊆ 𝑋 )
12 1 fvexi ⊢ 𝑋 ∈ V
13 12 ssex ⊢ ( ran 𝐹 ⊆ 𝑋 → ran 𝐹 ∈ V )
14 10 11 13 3syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ran 𝐹 ∈ V )
15 elfzelz ⊢ ( 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) → 𝑦 ∈ ℤ )
16 15 adantl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → 𝑦 ∈ ℤ )
17 ovex ⊢ ( 𝑦 · 𝐴 ) ∈ V
18 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
19 4 18 elrnmpt1s ⊢ ( ( 𝑦 ∈ ℤ ∧ ( 𝑦 · 𝐴 ) ∈ V ) → ( 𝑦 · 𝐴 ) ∈ ran 𝐹 )
20 16 17 19 sylancl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( 𝑦 · 𝐴 ) ∈ ran 𝐹 )
21 20 ralrimiva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ∀ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( 𝑦 · 𝐴 ) ∈ ran 𝐹 )
22 zmodfz ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) )
23 22 ancoms ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∧ 𝑥 ∈ ℤ ) → ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) )
24 23 adantll ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) )
25 simpllr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
26 simplr ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → 𝑥 ∈ ℤ )
27 15 adantl ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → 𝑦 ∈ ℤ )
28 moddvds ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ) )
29 25 26 27 28 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ) )
30 27 zred ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → 𝑦 ∈ ℝ )
31 25 nnrpd ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ )
32 0z ⊢ 0 ∈ ℤ
33 nnz ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
34 33 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
35 34 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
36 elfzm11 ⊢ ( ( 0 ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℤ ) → ( 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ↔ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < ( 𝑂 ‘ 𝐴 ) ) ) )
37 32 35 36 sylancr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ↔ ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < ( 𝑂 ‘ 𝐴 ) ) ) )
38 37 biimpa ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( 𝑦 ∈ ℤ ∧ 0 ≤ 𝑦 ∧ 𝑦 < ( 𝑂 ‘ 𝐴 ) ) )
39 38 simp2d ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → 0 ≤ 𝑦 )
40 38 simp3d ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → 𝑦 < ( 𝑂 ‘ 𝐴 ) )
41 modid ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ ) ∧ ( 0 ≤ 𝑦 ∧ 𝑦 < ( 𝑂 ‘ 𝐴 ) ) ) → ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) = 𝑦 )
42 30 31 39 40 41 syl22anc ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) = 𝑦 )
43 42 eqeq2d ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) ↔ ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) = 𝑦 ) )
44 eqcom ⊢ ( ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) = 𝑦 ↔ 𝑦 = ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) )
45 43 44 bitrdi ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) ↔ 𝑦 = ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) ) )
46 simp-4l ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → 𝐺 ∈ Grp )
47 simp-4r ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → 𝐴 ∈ 𝑋 )
48 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
49 1 2 3 48 odcong ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ) )
50 46 47 26 27 49 syl112anc ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ) )
51 29 45 50 3bitr3rd ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ) → ( ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ↔ 𝑦 = ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) ) )
52 51 ralrimiva ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ∀ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ↔ 𝑦 = ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) ) )
53 reu6i ⊢ ( ( ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ∧ ∀ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ↔ 𝑦 = ( 𝑥 mod ( 𝑂 ‘ 𝐴 ) ) ) ) → ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
54 24 52 53 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ℤ ) → ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
55 54 ralrimiva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ∀ 𝑥 ∈ ℤ ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
56 ovex ⊢ ( 𝑥 · 𝐴 ) ∈ V
57 56 rgenw ⊢ ∀ 𝑥 ∈ ℤ ( 𝑥 · 𝐴 ) ∈ V
58 eqeq1 ⊢ ( 𝑧 = ( 𝑥 · 𝐴 ) → ( 𝑧 = ( 𝑦 · 𝐴 ) ↔ ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ) )
59 58 reubidv ⊢ ( 𝑧 = ( 𝑥 · 𝐴 ) → ( ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) 𝑧 = ( 𝑦 · 𝐴 ) ↔ ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ) )
60 4 59 ralrnmptw ⊢ ( ∀ 𝑥 ∈ ℤ ( 𝑥 · 𝐴 ) ∈ V → ( ∀ 𝑧 ∈ ran 𝐹 ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) 𝑧 = ( 𝑦 · 𝐴 ) ↔ ∀ 𝑥 ∈ ℤ ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ) )
61 57 60 ax-mp ⊢ ( ∀ 𝑧 ∈ ran 𝐹 ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) 𝑧 = ( 𝑦 · 𝐴 ) ↔ ∀ 𝑥 ∈ ℤ ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
62 55 61 sylibr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ∀ 𝑧 ∈ ran 𝐹 ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) 𝑧 = ( 𝑦 · 𝐴 ) )
63 eqid ⊢ ( 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ↦ ( 𝑦 · 𝐴 ) ) = ( 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ↦ ( 𝑦 · 𝐴 ) )
64 63 f1ompt ⊢ ( ( 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ↦ ( 𝑦 · 𝐴 ) ) : ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) –1-1-onto→ ran 𝐹 ↔ ( ∀ 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ( 𝑦 · 𝐴 ) ∈ ran 𝐹 ∧ ∀ 𝑧 ∈ ran 𝐹 ∃! 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) 𝑧 = ( 𝑦 · 𝐴 ) ) )
65 21 62 64 sylanbrc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ↦ ( 𝑦 · 𝐴 ) ) : ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) –1-1-onto→ ran 𝐹 )
66 f1oen2g ⊢ ( ( ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ∈ Fin ∧ ran 𝐹 ∈ V ∧ ( 𝑦 ∈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ↦ ( 𝑦 · 𝐴 ) ) : ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) –1-1-onto→ ran 𝐹 ) → ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ≈ ran 𝐹 )
67 5 14 65 66 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ≈ ran 𝐹 )
68 enfi ⊢ ( ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ≈ ran 𝐹 → ( ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ∈ Fin ↔ ran 𝐹 ∈ Fin ) )
69 67 68 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ∈ Fin ↔ ran 𝐹 ∈ Fin ) )
70 5 69 mpbid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ran 𝐹 ∈ Fin )
71 70 iftrued ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → if ( ran 𝐹 ∈ Fin , ( ♯ ‘ ran 𝐹 ) , 0 ) = ( ♯ ‘ ran 𝐹 ) )
72 fz01en ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ → ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ≈ ( 1 ... ( 𝑂 ‘ 𝐴 ) ) )
73 ensym ⊢ ( ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ≈ ( 1 ... ( 𝑂 ‘ 𝐴 ) ) → ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ≈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) )
74 34 72 73 3syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ≈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) )
75 entr ⊢ ( ( ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ≈ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ∧ ( 0 ... ( ( 𝑂 ‘ 𝐴 ) − 1 ) ) ≈ ran 𝐹 ) → ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ≈ ran 𝐹 )
76 74 67 75 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ≈ ran 𝐹 )
77 fzfid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ∈ Fin )
78 hashen ⊢ ( ( ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ∈ Fin ∧ ran 𝐹 ∈ Fin ) → ( ( ♯ ‘ ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ) = ( ♯ ‘ ran 𝐹 ) ↔ ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ≈ ran 𝐹 ) )
79 77 70 78 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ♯ ‘ ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ) = ( ♯ ‘ ran 𝐹 ) ↔ ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ≈ ran 𝐹 ) )
80 76 79 mpbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ) = ( ♯ ‘ ran 𝐹 ) )
81 nnnn0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
82 81 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
83 hashfz1 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ) = ( 𝑂 ‘ 𝐴 ) )
84 82 83 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( 𝑂 ‘ 𝐴 ) ) ) = ( 𝑂 ‘ 𝐴 ) )
85 71 80 84 3eqtr2rd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) = if ( ran 𝐹 ∈ Fin , ( ♯ ‘ ran 𝐹 ) , 0 ) )
86 simp3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) = 0 )
87 1 2 3 4 odinf ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ¬ ran 𝐹 ∈ Fin )
88 87 iffalsed ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → if ( ran 𝐹 ∈ Fin , ( ♯ ‘ ran 𝐹 ) , 0 ) = 0 )
89 86 88 eqtr4d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) = if ( ran 𝐹 ∈ Fin , ( ♯ ‘ ran 𝐹 ) , 0 ) )
90 89 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑂 ‘ 𝐴 ) = if ( ran 𝐹 ∈ Fin , ( ♯ ‘ ran 𝐹 ) , 0 ) )
91 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
92 91 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
93 elnn0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
94 92 93 sylib ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
95 85 90 94 mpjaodan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = if ( ran 𝐹 ∈ Fin , ( ♯ ‘ ran 𝐹 ) , 0 ) )