This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prmcyg

Description: A group with prime order is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypothesis cygctb.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion prmcyg ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) → 𝐺 ∈ CycGrp )

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 1nprm ⊢ ¬ 1 ∈ ℙ
3 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } ) → 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } )
4 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5 1 4 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
6 5 snssd ⊢ ( 𝐺 ∈ Grp → { ( 0g ‘ 𝐺 ) } ⊆ 𝐵 )
7 6 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } ) → { ( 0g ‘ 𝐺 ) } ⊆ 𝐵 )
8 3 7 eqssd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } ) → 𝐵 = { ( 0g ‘ 𝐺 ) } )
9 8 fveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } ) → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) )
10 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
11 hashsng ⊢ ( ( 0g ‘ 𝐺 ) ∈ V → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1 )
12 10 11 ax-mp ⊢ ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1
13 9 12 eqtrdi ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } ) → ( ♯ ‘ 𝐵 ) = 1 )
14 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } ) → ( ♯ ‘ 𝐵 ) ∈ ℙ )
15 13 14 eqeltrrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } ) → 1 ∈ ℙ )
16 15 ex ⊢ ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) → ( 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } → 1 ∈ ℙ ) )
17 2 16 mtoi ⊢ ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) → ¬ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } )
18 nss ⊢ ( ¬ 𝐵 ⊆ { ( 0g ‘ 𝐺 ) } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) )
19 17 18 sylib ⊢ ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) )
20 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
21 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → 𝐺 ∈ Grp )
22 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → 𝑥 ∈ 𝐵 )
23 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } )
24 20 4 1 odeq1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 1 ↔ 𝑥 = ( 0g ‘ 𝐺 ) ) )
25 21 22 24 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 1 ↔ 𝑥 = ( 0g ‘ 𝐺 ) ) )
26 velsn ⊢ ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ↔ 𝑥 = ( 0g ‘ 𝐺 ) )
27 25 26 bitr4di ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 1 ↔ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) )
28 23 27 mtbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ¬ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 1 )
29 prmnn ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℙ → ( ♯ ‘ 𝐵 ) ∈ ℕ )
30 29 ad2antlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
31 30 nnnn0d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
32 1 fvexi ⊢ 𝐵 ∈ V
33 hashclb ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) )
34 32 33 ax-mp ⊢ ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
35 31 34 sylibr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → 𝐵 ∈ Fin )
36 1 20 oddvds2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) )
37 21 35 22 36 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) )
38 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ♯ ‘ 𝐵 ) ∈ ℙ )
39 1 20 odcl2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ )
40 21 35 22 39 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ )
41 dvdsprime ⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℙ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∨ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 1 ) ) )
42 38 40 41 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∨ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 1 ) ) )
43 37 42 mpbid ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∨ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 1 ) )
44 43 ord ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ¬ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 1 ) )
45 28 44 mt3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) )
46 1 20 21 22 45 iscygodd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) ) → 𝐺 ∈ CycGrp )
47 19 46 exlimddv ⊢ ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) → 𝐺 ∈ CycGrp )