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 ) )