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={\mathrm{Base}}_G$$
	finsubmsubg.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	finsubmsubg.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left(G\right)$$
	finsubmsubg.1	$$⊢\phi \to B\in \mathrm{Fin}$$
Assertion	finsubmsubg	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		finsubmsubg.b	$$⊢B={\mathrm{Base}}_G$$
2		finsubmsubg.g	$$⊢\phi \to G\in \mathrm{Grp}$$
3		finsubmsubg.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left(G\right)$$
4		finsubmsubg.1	$$⊢\phi \to B\in \mathrm{Fin}$$
5		eqid	$$⊢\mathrm{od}\left(G\right)=\mathrm{od}\left(G\right)$$
6	2	adantr	$$⊢\left(\phi \wedge a\in S\right)\to G\in \mathrm{Grp}$$
7	4	adantr	$$⊢\left(\phi \wedge a\in S\right)\to B\in \mathrm{Fin}$$
8	1	submss	$$⊢S\in \mathrm{SubMnd}\left(G\right)\to S\subseteq B$$
9	3 8	syl	$$⊢\phi \to S\subseteq B$$
10	9	sselda	$$⊢\left(\phi \wedge a\in S\right)\to a\in B$$
11	1 5	odcl2	$$⊢\left(G\in \mathrm{Grp}\wedge B\in \mathrm{Fin}\wedge a\in B\right)\to \mathrm{od}\left(G\right)\left(a\right)\in \mathbb{N}$$
12	6 7 10 11	syl3anc	$$⊢\left(\phi \wedge a\in S\right)\to \mathrm{od}\left(G\right)\left(a\right)\in \mathbb{N}$$
13	12	ralrimiva	$$⊢\phi \to \forall a\in S\mathrm{od}\left(G\right)\left(a\right)\in \mathbb{N}$$
14	5 2 3 13	finodsubmsubg	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$