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