Theorem prmgrpsimpgd

Description: A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	prmgrpsimpgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	prmgrpsimpgd.2	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	prmgrpsimpgd.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℙ )
Assertion	prmgrpsimpgd	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )

Proof

Step	Hyp	Ref	Expression
1		prmgrpsimpgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		prmgrpsimpgd.2	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		prmgrpsimpgd.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℙ )
4		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5		fveq2	⊢ ( { ( 0g ‘ 𝐺 ) } = 𝐵 → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ 𝐵 ) )
6	5	adantl	⊢ ( ( 𝜑 ∧ { ( 0g ‘ 𝐺 ) } = 𝐵 ) → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ 𝐵 ) )
7	4	fvexi	⊢ ( 0g ‘ 𝐺 ) ∈ V
8		hashsng	⊢ ( ( 0g ‘ 𝐺 ) ∈ V → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1 )
9	7 8	mp1i	⊢ ( ( 𝜑 ∧ { ( 0g ‘ 𝐺 ) } = 𝐵 ) → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1 )
10	6 9	eqtr3d	⊢ ( ( 𝜑 ∧ { ( 0g ‘ 𝐺 ) } = 𝐵 ) → ( ♯ ‘ 𝐵 ) = 1 )
11	3	adantr	⊢ ( ( 𝜑 ∧ { ( 0g ‘ 𝐺 ) } = 𝐵 ) → ( ♯ ‘ 𝐵 ) ∈ ℙ )
12	10 11	eqeltrrd	⊢ ( ( 𝜑 ∧ { ( 0g ‘ 𝐺 ) } = 𝐵 ) → 1 ∈ ℙ )
13		1nprm	⊢ ¬ 1 ∈ ℙ
14	13	a1i	⊢ ( ( 𝜑 ∧ { ( 0g ‘ 𝐺 ) } = 𝐵 ) → ¬ 1 ∈ ℙ )
15	12 14	pm2.65da	⊢ ( 𝜑 → ¬ { ( 0g ‘ 𝐺 ) } = 𝐵 )
16		nsgsubg	⊢ ( 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) )
17		eqid	⊢ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐵 )
18	1	fvexi	⊢ 𝐵 ∈ V
19	18	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
20		prmnn	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℙ → ( ♯ ‘ 𝐵 ) ∈ ℕ )
21	3 20	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )
22	21	nnnn0d	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
23		hashvnfin	⊢ ( ( 𝐵 ∈ V ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐵 ) → 𝐵 ∈ Fin ) )
24	19 22 23	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) = ( ♯ ‘ 𝐵 ) → 𝐵 ∈ Fin ) )
25	17 24	mpi	⊢ ( 𝜑 → 𝐵 ∈ Fin )
26	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) → 𝐵 ∈ Fin )
27	1	subgss	⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥 ⊆ 𝐵 )
28	27	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) → 𝑥 ⊆ 𝐵 )
29		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) )
30	26 28 29	phphashrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) → 𝑥 = 𝐵 )
31	30	olcd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ) → ( 𝑥 = { ( 0g ‘ 𝐺 ) } ∨ 𝑥 = 𝐵 ) )
32		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) → ( ♯ ‘ 𝑥 ) = 1 )
33	4	subg0cl	⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑥 )
34	33	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) → ( 0g ‘ 𝐺 ) ∈ 𝑥 )
35		vex	⊢ 𝑥 ∈ V
36	35	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) → 𝑥 ∈ V )
37	32 34 36	hash1elsn	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) → 𝑥 = { ( 0g ‘ 𝐺 ) } )
38	37	orcd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = 1 ) → ( 𝑥 = { ( 0g ‘ 𝐺 ) } ∨ 𝑥 = 𝐵 ) )
39	1	lagsubg	⊢ ( ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) )
40	25 39	sylan2	⊢ ( ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝜑 ) → ( ♯ ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) )
41	40	ancoms	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ♯ ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) )
42	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℙ )
43	25	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐵 ∈ Fin )
44	27	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑥 ⊆ 𝐵 )
45	43 44	ssfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑥 ∈ Fin )
46		hashcl	⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
47	45 46	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
48	33	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑥 )
49	35	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑥 ∈ V )
50	48 49	hashelne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ¬ ( ♯ ‘ 𝑥 ) = 0 )
51	50	neqned	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ♯ ‘ 𝑥 ) ≠ 0 )
52		elnnne0	⊢ ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑥 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑥 ) ≠ 0 ) )
53	47 51 52	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ )
54		dvdsprime	⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℙ ∧ ( ♯ ‘ 𝑥 ) ∈ ℕ ) → ( ( ♯ ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∨ ( ♯ ‘ 𝑥 ) = 1 ) ) )
55	42 53 54	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑥 ) ∥ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∨ ( ♯ ‘ 𝑥 ) = 1 ) ) )
56	41 55	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐵 ) ∨ ( ♯ ‘ 𝑥 ) = 1 ) )
57	31 38 56	mpjaodan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 = { ( 0g ‘ 𝐺 ) } ∨ 𝑥 = 𝐵 ) )
58	16 57	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑥 = { ( 0g ‘ 𝐺 ) } ∨ 𝑥 = 𝐵 ) )
59	1 4 2 15 58	2nsgsimpgd	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )