ablsimpgprmd

Description: An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	ablsimpgprmd.1	$⊢ B = {Base}_{G}$
	ablsimpgprmd.2	$⊢ φ \to G \in Abel$
	ablsimpgprmd.3	$⊢ φ \to G \in SimpGrp$
Assertion	ablsimpgprmd	$⊢ φ \to \|B\| \in ℙ$

Proof

Step	Hyp	Ref	Expression
1		ablsimpgprmd.1	$⊢ B = {Base}_{G}$
2		ablsimpgprmd.2	$⊢ φ \to G \in Abel$
3		ablsimpgprmd.3	$⊢ φ \to G \in SimpGrp$
4		simpr	$⊢ (φ \land \|B\| = 1) \to \|B\| = 1$
5	3	simpggrpd	$⊢ φ \to G \in Grp$
6		eqid	$⊢ 0_{G} = 0_{G}$
7	1 6	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
8	5 7	syl	$⊢ φ \to 0_{G} \in B$
9	8	adantr	$⊢ (φ \land \|B\| = 1) \to 0_{G} \in B$
10	1 2 3	ablsimpgfind	$⊢ φ \to B \in Fin$
11	10	adantr	$⊢ (φ \land \|B\| = 1) \to B \in Fin$
12	4 9 11	hash1elsn	$⊢ (φ \land \|B\| = 1) \to B = \{0_{G}\}$
13	3	adantr	$⊢ (φ \land \|B\| = 1) \to G \in SimpGrp$
14	1 6 13	simpgntrivd	$⊢ (φ \land \|B\| = 1) \to \neg B = \{0_{G}\}$
15	12 14	pm2.65da	$⊢ φ \to \neg \|B\| = 1$
16	1 5 10	hashfingrpnn	$⊢ φ \to \|B\| \in ℕ$
17		elnn1uz2	$⊢ \|B\| \in ℕ \leftrightarrow (\|B\| = 1 \lor \|B\| \in ℤ_{\geq 2})$
18	16 17	sylib	$⊢ φ \to (\|B\| = 1 \lor \|B\| \in ℤ_{\geq 2})$
19	18	ord	$⊢ φ \to (\neg \|B\| = 1 \to \|B\| \in ℤ_{\geq 2})$
20	15 19	mpd	$⊢ φ \to \|B\| \in ℤ_{\geq 2}$
21	2 3	ablsimpgcygd	$⊢ φ \to G \in CycGrp$
22	21	3ad2ant1	$⊢ (φ \land y \in ℕ \land y ∥ \|B\|) \to G \in CycGrp$
23		simp3	$⊢ (φ \land y \in ℕ \land y ∥ \|B\|) \to y ∥ \|B\|$
24	10	3ad2ant1	$⊢ (φ \land y \in ℕ \land y ∥ \|B\|) \to B \in Fin$
25		simp2	$⊢ (φ \land y \in ℕ \land y ∥ \|B\|) \to y \in ℕ$
26	1 22 23 24 25	fincygsubgodexd	$⊢ (φ \land y \in ℕ \land y ∥ \|B\|) \to \exists x \in SubGrp (G) \|x\| = y$
27		simpl1	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to φ$
28	27 3	syl	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to G \in SimpGrp$
29		simprl	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to x \in SubGrp (G)$
30		ablnsg	$⊢ G \in Abel \to NrmSGrp (G) = SubGrp (G)$
31	27 2 30	3syl	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to NrmSGrp (G) = SubGrp (G)$
32	29 31	eleqtrrd	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to x \in NrmSGrp (G)$
33	1 6 28 32	simpgnsgeqd	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to (x = \{0_{G}\} \lor x = B)$
34		simpr	$⊢ (((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \land x = \{0_{G}\}) \to x = \{0_{G}\}$
35	34	fveq2d	$⊢ (((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \land x = \{0_{G}\}) \to \|x\| = \|\{0_{G}\}\|$
36		simplrr	$⊢ (((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \land x = \{0_{G}\}) \to \|x\| = y$
37	6	fvexi	$⊢ 0_{G} \in V$
38		hashsng	$⊢ 0_{G} \in V \to \|\{0_{G}\}\| = 1$
39	37 38	mp1i	$⊢ (((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \land x = \{0_{G}\}) \to \|\{0_{G}\}\| = 1$
40	35 36 39	3eqtr3d	$⊢ (((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \land x = \{0_{G}\}) \to y = 1$
41	40	ex	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to (x = \{0_{G}\} \to y = 1)$
42		simplrr	$⊢ (((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \land x = B) \to \|x\| = y$
43		simpr	$⊢ (((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \land x = B) \to x = B$
44	43	fveq2d	$⊢ (((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \land x = B) \to \|x\| = \|B\|$
45	42 44	eqtr3d	$⊢ (((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \land x = B) \to y = \|B\|$
46	45	ex	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to (x = B \to y = \|B\|)$
47	41 46	orim12d	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to ((x = \{0_{G}\} \lor x = B) \to (y = 1 \lor y = \|B\|))$
48	33 47	mpd	$⊢ ((φ \land y \in ℕ \land y ∥ \|B\|) \land (x \in SubGrp (G) \land \|x\| = y)) \to (y = 1 \lor y = \|B\|)$
49	26 48	rexlimddv	$⊢ (φ \land y \in ℕ \land y ∥ \|B\|) \to (y = 1 \lor y = \|B\|)$
50	49	3exp	$⊢ φ \to (y \in ℕ \to (y ∥ \|B\| \to (y = 1 \lor y = \|B\|)))$
51	50	ralrimiv	$⊢ φ \to \forall y \in ℕ (y ∥ \|B\| \to (y = 1 \lor y = \|B\|))$
52		isprm2	$⊢ \|B\| \in ℙ \leftrightarrow (\|B\| \in ℤ_{\geq 2} \land \forall y \in ℕ (y ∥ \|B\| \to (y = 1 \lor y = \|B\|)))$
53	20 51 52	sylanbrc	$⊢ φ \to \|B\| \in ℙ$

Metamath Proof Explorer

Theorem ablsimpgprmd

Proof