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 = Base G
ablsimpgfind.2 ⊢ φ → G ∈ Abel
ablsimpgfind.3 ⊢ φ → G ∈ SimpGrp
Assertion ablsimpgfind ⊢ φ → B ∈ Fin

Proof

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