This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem finsubmsubg

Description: A submonoid of a finite group is a subgroup. This does not extend to infinite groups, as the submonoid NN0 of the group ( ZZ , + ) shows. Note also that the union of a submonoid and its inverses need not be a submonoid, as the submonoid ( NN0 \ { 1 } ) of the group ( ZZ , + ) shows: 3 is in that submonoid, -2 is the inverse of 2, but 1 is not in their union. Or simply, the subgroup generated by ( NN0 \ { 1 } ) is ZZ , not ( ZZ \ { 1 , -u 1 } ) . (Contributed by SN, 31-Jan-2025)

Ref Expression
Hypotheses finsubmsubg.b 
|- B = ( Base ` G )
finsubmsubg.g 
|- ( ph -> G e. Grp )
finsubmsubg.s 
|- ( ph -> S e. ( SubMnd ` G ) )
finsubmsubg.1 
|- ( ph -> B e. Fin )
Assertion finsubmsubg 
|- ( ph -> S e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 finsubmsubg.b 
 |-  B = ( Base ` G )
2 finsubmsubg.g 
 |-  ( ph -> G e. Grp )
3 finsubmsubg.s 
 |-  ( ph -> S e. ( SubMnd ` G ) )
4 finsubmsubg.1 
 |-  ( ph -> B e. Fin )
5 eqid 
 |-  ( od ` G ) = ( od ` G )
6 2 adantr 
 |-  ( ( ph /\ a e. S ) -> G e. Grp )
7 4 adantr 
 |-  ( ( ph /\ a e. S ) -> B e. Fin )
8 1 submss 
 |-  ( S e. ( SubMnd ` G ) -> S C_ B )
9 3 8 syl 
 |-  ( ph -> S C_ B )
10 9 sselda 
 |-  ( ( ph /\ a e. S ) -> a e. B )
11 1 5 odcl2 
 |-  ( ( G e. Grp /\ B e. Fin /\ a e. B ) -> ( ( od ` G ) ` a ) e. NN )
12 6 7 10 11 syl3anc 
 |-  ( ( ph /\ a e. S ) -> ( ( od ` G ) ` a ) e. NN )
13 12 ralrimiva 
 |-  ( ph -> A. a e. S ( ( od ` G ) ` a ) e. NN )
14 5 2 3 13 finodsubmsubg 
 |-  ( ph -> S e. ( SubGrp ` G ) )