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