Metamath Proof Explorer

Theorem odngen

Description: A cyclic subgroup of size ( OA ) has ( phi( OA ) ) generators. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses odhash.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
odhash.o ⊢ 𝑂 = ( od ‘ 𝐺 )
odhash.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion odngen ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) = ( ϕ ‘ ( 𝑂 ‘ 𝐴 ) ) )

Proof

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 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( 𝐾 ‘ { 𝐴 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝐴 ) } ) = ( ϕ ‘ ( 𝑂 ‘ 𝐴 ) ) )