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 )