Metamath Proof Explorer


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 abbi2dv ( ( 𝜑 ∧ ( 𝑥𝐵𝑥 ≠ ( 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 )