Theorem ablsimpgfind

Description: An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	ablsimpgfind.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ablsimpgfind.2	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	ablsimpgfind.3	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
Assertion	ablsimpgfind	⊢ ( 𝜑 → 𝐵 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		ablsimpgfind.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ablsimpgfind.2	⊢ ( 𝜑 → 𝐺 ∈ Abel )
3		ablsimpgfind.3	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
4		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ Fin ) → ¬ 𝐵 ∈ Fin )
5	4	iffalsed	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ Fin ) → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) = 0 )
6		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7	1 6 3	simpgnideld	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ¬ 𝑥 = ( 0g ‘ 𝐺 ) )
8		neqne	⊢ ( ¬ 𝑥 = ( 0g ‘ 𝐺 ) → 𝑥 ≠ ( 0g ‘ 𝐺 ) )
9	8	reximi	⊢ ( ∃ 𝑥 ∈ 𝐵 ¬ 𝑥 = ( 0g ‘ 𝐺 ) → ∃ 𝑥 ∈ 𝐵 𝑥 ≠ ( 0g ‘ 𝐺 ) )
10	7 9	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝑥 ≠ ( 0g ‘ 𝐺 ) )
11		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
12		eqid	⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
13	3	simpggrpd	⊢ ( 𝜑 → 𝐺 ∈ Grp )
14	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → 𝐺 ∈ Grp )
15		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → 𝑥 ∈ 𝐵 )
16	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐺 ∈ Abel )
17	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐺 ∈ SimpGrp )
18	15	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
19		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ≠ ( 0g ‘ 𝐺 ) )
20	19	neneqd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝑥 = ( 0g ‘ 𝐺 ) )
21		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
22	1 6 11 16 17 18 20 21	ablsimpg1gend	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) )
23	22	ex	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → ( 𝑦 ∈ 𝐵 → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) )
24		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ) → 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) )
25	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ) → 𝐺 ∈ Grp )
26		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ) → 𝑛 ∈ ℤ )
27	15	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ) → 𝑥 ∈ 𝐵 )
28	1 11 25 26 27	mulgcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ) → ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
29	24 28	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) ) → 𝑦 ∈ 𝐵 )
30	29	rexlimdvaa	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → ( ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) → 𝑦 ∈ 𝐵 ) )
31	23 30	impbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → ( 𝑦 ∈ 𝐵 ↔ ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) )
32	31	eqabdv	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → 𝐵 = { 𝑦 ∣ ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) } )
33		eqid	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) )
34	33	rnmpt	⊢ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = { 𝑦 ∣ ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) }
35	32 34	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → 𝐵 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) )
36	1 11 12 14 15 35	cycsubggenodd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
37	1 6 11 12 2 3	ablsimpgfindlem2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ≠ 0 )
38	1 6 11 12 2 3	ablsimpgfindlem1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 ( .g ‘ 𝐺 ) 𝑥 ) ≠ ( 0g ‘ 𝐺 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ≠ 0 )
39	37 38	pm2.61dane	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ≠ 0 )
40	39	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ≠ 0 )
41	36 40	eqnetrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝐺 ) ) ) → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ≠ 0 )
42	10 41	rexlimddv	⊢ ( 𝜑 → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ≠ 0 )
43	42	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ Fin ) → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ≠ 0 )
44	5 43	pm2.21ddne	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ Fin ) → ⊥ )
45	44	efald	⊢ ( 𝜑 → 𝐵 ∈ Fin )