Metamath Proof Explorer

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→ ( 𝐾 ‘ { 𝐴 } ) )