Metamath Proof Explorer

Theorem ablsimpgfind

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

Ref Expression
Hypotheses ablsimpgfind.1 ⊢B=BaseG
ablsimpgfind.2 ⊢φ→G∈Abel
ablsimpgfind.3 ⊢φ→G∈SimpGrp
Assertion ablsimpgfind ⊢φ→B∈Fin

Proof

Step Hyp Ref Expression
1 ablsimpgfind.1 ⊢B=BaseG
2 ablsimpgfind.2 ⊢φ→G∈Abel
3 ablsimpgfind.3 ⊢φ→G∈SimpGrp
4 simpr ⊢φ∧¬B∈Fin→¬B∈Fin
5 4 iffalsed ⊢φ∧¬B∈Fin→ifB∈FinB0=0
6 eqid ⊢0G=0G
7 1 6 3 simpgnideld ⊢φ→∃x∈B¬x=0G
8 neqne ⊢¬x=0G→x≠0G
9 8 reximi ⊢∃x∈B¬x=0G→∃x∈Bx≠0G
10 7 9 syl ⊢φ→∃x∈Bx≠0G
11 eqid ⊢⋅G=⋅G
12 eqid ⊢od⁡G=od⁡G
13 3 simpggrpd ⊢φ→G∈Grp
14 13 adantr ⊢φ∧x∈B∧x≠0G→G∈Grp
15 simprl ⊢φ∧x∈B∧x≠0G→x∈B
16 2 ad2antrr ⊢φ∧x∈B∧x≠0G∧y∈B→G∈Abel
17 3 ad2antrr ⊢φ∧x∈B∧x≠0G∧y∈B→G∈SimpGrp
18 15 adantr ⊢φ∧x∈B∧x≠0G∧y∈B→x∈B
19 simplrr ⊢φ∧x∈B∧x≠0G∧y∈B→x≠0G
20 19 neneqd ⊢φ∧x∈B∧x≠0G∧y∈B→¬x=0G
21 simpr ⊢φ∧x∈B∧x≠0G∧y∈B→y∈B
22 1 6 11 16 17 18 20 21 ablsimpg1gend ⊢φ∧x∈B∧x≠0G∧y∈B→∃n∈ℤy=n⋅Gx
23 22 ex ⊢φ∧x∈B∧x≠0G→y∈B→∃n∈ℤy=n⋅Gx
24 simprr ⊢φ∧x∈B∧x≠0G∧n∈ℤ∧y=n⋅Gx→y=n⋅Gx
25 13 ad2antrr ⊢φ∧x∈B∧x≠0G∧n∈ℤ∧y=n⋅Gx→G∈Grp
26 simprl ⊢φ∧x∈B∧x≠0G∧n∈ℤ∧y=n⋅Gx→n∈ℤ
27 15 adantr ⊢φ∧x∈B∧x≠0G∧n∈ℤ∧y=n⋅Gx→x∈B
28 1 11 25 26 27 mulgcld ⊢φ∧x∈B∧x≠0G∧n∈ℤ∧y=n⋅Gx→n⋅Gx∈B
29 24 28 eqeltrd ⊢φ∧x∈B∧x≠0G∧n∈ℤ∧y=n⋅Gx→y∈B
30 29 rexlimdvaa ⊢φ∧x∈B∧x≠0G→∃n∈ℤy=n⋅Gx→y∈B
31 23 30 impbid ⊢φ∧x∈B∧x≠0G→y∈B↔∃n∈ℤy=n⋅Gx
32 31 eqabdv ⊢φ∧x∈B∧x≠0G→B=y|∃n∈ℤy=n⋅Gx
33 eqid ⊢n∈ℤ⟼n⋅Gx=n∈ℤ⟼n⋅Gx
34 33 rnmpt ⊢ran⁡n∈ℤ⟼n⋅Gx=y|∃n∈ℤy=n⋅Gx
35 32 34 eqtr4di ⊢φ∧x∈B∧x≠0G→B=ran⁡n∈ℤ⟼n⋅Gx
36 1 11 12 14 15 35 cycsubggenodd ⊢φ∧x∈B∧x≠0G→od⁡G⁡x=ifB∈FinB0
37 1 6 11 12 2 3 ablsimpgfindlem2 ⊢φ∧x∈B∧2⋅Gx=0G→od⁡G⁡x≠0
38 1 6 11 12 2 3 ablsimpgfindlem1 ⊢φ∧x∈B∧2⋅Gx≠0G→od⁡G⁡x≠0
39 37 38 pm2.61dane ⊢φ∧x∈B→od⁡G⁡x≠0
40 39 adantrr ⊢φ∧x∈B∧x≠0G→od⁡G⁡x≠0
41 36 40 eqnetrrd ⊢φ∧x∈B∧x≠0G→ifB∈FinB0≠0
42 10 41 rexlimddv ⊢φ→ifB∈FinB0≠0
43 42 adantr ⊢φ∧¬B∈Fin→ifB∈FinB0≠0
44 5 43 pm2.21ddne ⊢φ∧¬B∈Fin→⊥
45 44 efald ⊢φ→B∈Fin