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 
|- ( ph -> G e. Grp )
finodsubmsubg.s 
|- ( ph -> S e. ( SubMnd ` G ) )
finodsubmsubg.1 
|- ( ph -> A. a e. S ( O ` a ) e. NN )
Assertion finodsubmsubg 
|- ( ph -> S e. ( SubGrp ` G ) )

Proof

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