Theorem odf1o2

Description: An element with nonzero order has as many multiples as its order. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	odf1o1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odf1o1.t	⊢ · = ( .g ‘ 𝐺 )
	odf1o1.o	⊢ 𝑂 = ( od ‘ 𝐺 )
	odf1o1.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion	odf1o2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		odf1o1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odf1o1.t	⊢ · = ( .g ‘ 𝐺 )
3		odf1o1.o	⊢ 𝑂 = ( od ‘ 𝐺 )
4		odf1o1.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
5		simpl1	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → 𝐺 ∈ Grp )
6		elfzoelz	⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) → 𝑥 ∈ ℤ )
7	6	adantl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → 𝑥 ∈ ℤ )
8		simpl2	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → 𝐴 ∈ 𝑋 )
9	1 2	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 )
10	5 7 8 9	syl3anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 )
11	10	ex	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 ) )
12		simpl3	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
13	12	nncnd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℂ )
14	13	subid1d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → ( ( 𝑂 ‘ 𝐴 ) − 0 ) = ( 𝑂 ‘ 𝐴 ) )
15	14	breq1d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → ( ( ( 𝑂 ‘ 𝐴 ) − 0 ) ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ) )
16		fzocongeq	⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → ( ( ( 𝑂 ‘ 𝐴 ) − 0 ) ∥ ( 𝑥 − 𝑦 ) ↔ 𝑥 = 𝑦 ) )
17	16	adantl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → ( ( ( 𝑂 ‘ 𝐴 ) − 0 ) ∥ ( 𝑥 − 𝑦 ) ↔ 𝑥 = 𝑦 ) )
18		simpl1	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → 𝐺 ∈ Grp )
19		simpl2	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → 𝐴 ∈ 𝑋 )
20	6	ad2antrl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → 𝑥 ∈ ℤ )
21		elfzoelz	⊢ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) → 𝑦 ∈ ℤ )
22	21	ad2antll	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → 𝑦 ∈ ℤ )
23		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
24	1 3 2 23	odcong	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ) )
25	18 19 20 22 24	syl112anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ) )
26	15 17 25	3bitr3rd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ) → ( ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ↔ 𝑥 = 𝑦 ) )
27	26	ex	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → ( ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ↔ 𝑥 = 𝑦 ) ) )
28	11 27	dom2lem	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1→ 𝑋 )
29		f1fn	⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1→ 𝑋 → ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) Fn ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) )
30	28 29	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) Fn ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) )
31		resss	⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) ↾ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) ⊆ ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
32	6	ssriv	⊢ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ⊆ ℤ
33		resmpt	⊢ ( ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ⊆ ℤ → ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) ↾ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) )
34	32 33	ax-mp	⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) ↾ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) )
35		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
36	35	cbvmptv	⊢ ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) = ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) )
37	31 34 36	3sstr3i	⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) ⊆ ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) )
38		rnss	⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) ⊆ ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) ) → ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) ⊆ ran ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) ) )
39	37 38	mp1i	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) ⊆ ran ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) ) )
40		simpr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) → 𝑦 ∈ ℤ )
41		simpl3	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
42		zmodfzo	⊢ ( ( 𝑦 ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) )
43	40 41 42	syl2anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) → ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) )
44	1 3 2 23	odmod	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑦 · 𝐴 ) )
45	44	3an1rs	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑦 · 𝐴 ) )
46	45	eqcomd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) → ( 𝑦 · 𝐴 ) = ( ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
47		oveq1	⊢ ( 𝑥 = ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) → ( 𝑥 · 𝐴 ) = ( ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
48	47	rspceeqv	⊢ ( ( ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ ( 𝑦 · 𝐴 ) = ( ( 𝑦 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ∃ 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ( 𝑦 · 𝐴 ) = ( 𝑥 · 𝐴 ) )
49	43 46 48	syl2anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) → ∃ 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ( 𝑦 · 𝐴 ) = ( 𝑥 · 𝐴 ) )
50		ovex	⊢ ( 𝑦 · 𝐴 ) ∈ V
51		eqid	⊢ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) )
52	51	elrnmpt	⊢ ( ( 𝑦 · 𝐴 ) ∈ V → ( ( 𝑦 · 𝐴 ) ∈ ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ( 𝑦 · 𝐴 ) = ( 𝑥 · 𝐴 ) ) )
53	50 52	ax-mp	⊢ ( ( 𝑦 · 𝐴 ) ∈ ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) ↔ ∃ 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ( 𝑦 · 𝐴 ) = ( 𝑥 · 𝐴 ) )
54	49 53	sylibr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ℤ ) → ( 𝑦 · 𝐴 ) ∈ ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) )
55	54	fmpttd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) ) : ℤ ⟶ ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) )
56	55	frnd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ran ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) ) ⊆ ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) )
57	39 56	eqssd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) = ran ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) ) )
58		eqid	⊢ ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) ) = ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) )
59	1 2 58 4	cycsubg2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐾 ‘ { 𝐴 } ) = ran ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) ) )
60	59	3adant3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝐾 ‘ { 𝐴 } ) = ran ( 𝑦 ∈ ℤ ↦ ( 𝑦 · 𝐴 ) ) )
61	57 60	eqtr4d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) = ( 𝐾 ‘ { 𝐴 } ) )
62		df-fo	⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –onto→ ( 𝐾 ‘ { 𝐴 } ) ↔ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) Fn ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ ran ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) = ( 𝐾 ‘ { 𝐴 } ) ) )
63	30 61 62	sylanbrc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –onto→ ( 𝐾 ‘ { 𝐴 } ) )
64		df-f1	⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1→ 𝑋 ↔ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ⟶ 𝑋 ∧ Fun ◡ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) ) )
65	64	simprbi	⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1→ 𝑋 → Fun ◡ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) )
66	28 65	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → Fun ◡ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) )
67		dff1o3	⊢ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) ↔ ( ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –onto→ ( 𝐾 ‘ { 𝐴 } ) ∧ Fun ◡ ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) ) )
68	63 66 67	sylanbrc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑥 · 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) )