Step |
Hyp |
Ref |
Expression |
1 |
|
odhash.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
odhash.o |
⊢ 𝑂 = ( od ‘ 𝐺 ) |
3 |
|
odhash.k |
⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) |
4 |
|
eqid |
⊢ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) |
5 |
4
|
mptpreima |
⊢ ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) “ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) = { 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } } |
6 |
5
|
fveq2i |
⊢ ( ♯ ‘ ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) “ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } } ) |
7 |
|
eqid |
⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 ) |
8 |
1 7 2 3
|
odf1o2 |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) ) |
9 |
|
f1ocnv |
⊢ ( ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) → ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 𝐾 ‘ { 𝐴 } ) –1-1-onto→ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) |
10 |
|
f1of1 |
⊢ ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 𝐾 ‘ { 𝐴 } ) –1-1-onto→ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) → ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 𝐾 ‘ { 𝐴 } ) –1-1→ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) |
11 |
8 9 10
|
3syl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 𝐾 ‘ { 𝐴 } ) –1-1→ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) |
12 |
|
ssrab2 |
⊢ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ⊆ ( 𝐾 ‘ { 𝐴 } ) |
13 |
|
fvex |
⊢ ( 𝐾 ‘ { 𝐴 } ) ∈ V |
14 |
13
|
rabex |
⊢ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ∈ V |
15 |
14
|
f1imaen |
⊢ ( ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 𝐾 ‘ { 𝐴 } ) –1-1→ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ⊆ ( 𝐾 ‘ { 𝐴 } ) ) → ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) “ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) ≈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) |
16 |
|
hasheni |
⊢ ( ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) “ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) ≈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } → ( ♯ ‘ ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) “ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) ) = ( ♯ ‘ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) ) |
17 |
15 16
|
syl |
⊢ ( ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) : ( 𝐾 ‘ { 𝐴 } ) –1-1→ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∧ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ⊆ ( 𝐾 ‘ { 𝐴 } ) ) → ( ♯ ‘ ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) “ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) ) = ( ♯ ‘ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) ) |
18 |
11 12 17
|
sylancl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( ◡ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ↦ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) “ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) ) = ( ♯ ‘ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) ) |
19 |
|
simpl1 |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → 𝐺 ∈ Grp ) |
20 |
|
simpl2 |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → 𝐴 ∈ 𝑋 ) |
21 |
|
elfzoelz |
⊢ ( 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) → 𝑦 ∈ ℤ ) |
22 |
21
|
adantl |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → 𝑦 ∈ ℤ ) |
23 |
1 7 3
|
cycsubg2cl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℤ ) → ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) ) |
24 |
19 20 22 23
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) ) |
25 |
|
fveqeq2 |
⊢ ( 𝑥 = ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) → ( ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑂 ‘ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ) ) |
26 |
25
|
elrab3 |
⊢ ( ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) → ( ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ↔ ( 𝑂 ‘ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ) ) |
27 |
24 26
|
syl |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → ( ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ↔ ( 𝑂 ‘ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ) ) |
28 |
|
simpl3 |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) |
29 |
1 2 7
|
odmulgeq |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑦 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ) |
30 |
19 20 22 28 29
|
syl31anc |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → ( ( 𝑂 ‘ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑦 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ) |
31 |
27 30
|
bitrd |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ) → ( ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ↔ ( 𝑦 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ) |
32 |
31
|
rabbidva |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → { 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } } = { 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∣ ( 𝑦 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 } ) |
33 |
32
|
fveq2d |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } } ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∣ ( 𝑦 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 } ) ) |
34 |
|
dfphi2 |
⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( ϕ ‘ ( 𝑂 ‘ 𝐴 ) ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∣ ( 𝑦 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 } ) ) |
35 |
34
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ϕ ‘ ( 𝑂 ‘ 𝐴 ) ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∣ ( 𝑦 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 } ) ) |
36 |
33 35
|
eqtr4d |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑂 ‘ 𝐴 ) ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝐴 ) ∈ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } } ) = ( ϕ ‘ ( 𝑂 ‘ 𝐴 ) ) ) |
37 |
6 18 36
|
3eqtr3a |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) = ( ϕ ‘ ( 𝑂 ‘ 𝐴 ) ) ) |