Metamath Proof Explorer


Theorem finodsubmsubg

Description: A submonoid whose elements have finite order is a subgroup. (Contributed by SN, 31-Jan-2025)

Ref Expression
Hypotheses finodsubmsubg.o O = od G
finodsubmsubg.g φ G Grp
finodsubmsubg.s φ S SubMnd G
finodsubmsubg.1 φ a S O a
Assertion finodsubmsubg φ S SubGrp G

Proof

Step Hyp Ref Expression
1 finodsubmsubg.o O = od G
2 finodsubmsubg.g φ G Grp
3 finodsubmsubg.s φ S SubMnd G
4 finodsubmsubg.1 φ a S O a
5 eqid Base G = Base G
6 eqid G = G
7 eqid inv g G = inv g G
8 2 adantr φ a S G Grp
9 5 submss S SubMnd G S Base G
10 3 9 syl φ S Base G
11 10 sselda φ a S a Base G
12 5 1 6 7 8 11 odm1inv φ a S O a 1 G a = inv g G a
13 12 adantr φ a S O a O a 1 G a = inv g G a
14 eqid Base G 𝑠 S = Base G 𝑠 S
15 eqid G 𝑠 S = G 𝑠 S
16 eqid G 𝑠 S = G 𝑠 S
17 16 submmnd S SubMnd G G 𝑠 S Mnd
18 3 17 syl φ G 𝑠 S Mnd
19 18 ad2antrr φ a S O a G 𝑠 S Mnd
20 nnm1nn0 O a O a 1 0
21 20 adantl φ a S O a O a 1 0
22 simplr φ a S O a a S
23 16 5 ressbas2 S Base G S = Base G 𝑠 S
24 10 23 syl φ S = Base G 𝑠 S
25 24 ad2antrr φ a S O a S = Base G 𝑠 S
26 22 25 eleqtrd φ a S O a a Base G 𝑠 S
27 14 15 19 21 26 mulgnn0cld φ a S O a O a 1 G 𝑠 S a Base G 𝑠 S
28 3 ad2antrr φ a S O a S SubMnd G
29 6 16 15 submmulg S SubMnd G O a 1 0 a S O a 1 G a = O a 1 G 𝑠 S a
30 28 21 22 29 syl3anc φ a S O a O a 1 G a = O a 1 G 𝑠 S a
31 27 30 25 3eltr4d φ a S O a O a 1 G a S
32 13 31 eqeltrrd φ a S O a inv g G a S
33 32 ex φ a S O a inv g G a S
34 33 ralimdva φ a S O a a S inv g G a S
35 4 34 mpd φ a S inv g G a S
36 7 issubg3 G Grp S SubGrp G S SubMnd G a S inv g G a S
37 2 36 syl φ S SubGrp G S SubMnd G a S inv g G a S
38 3 35 37 mpbir2and φ S SubGrp G