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 ) )