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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	finsubmsubg.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	finsubmsubg.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
	finsubmsubg.1	⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion	finsubmsubg	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		finsubmsubg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		finsubmsubg.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		finsubmsubg.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
4		finsubmsubg.1	⊢ ( 𝜑 → 𝐵 ∈ Fin )
5		eqid	⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐺 ∈ Grp )
7	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐵 ∈ Fin )
8	1	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )
9	3 8	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
10	9	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝐵 )
11	1 5	odcl2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑎 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑎 ) ∈ ℕ )
12	6 7 10 11	syl3anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( od ‘ 𝐺 ) ‘ 𝑎 ) ∈ ℕ )
13	12	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ( ( od ‘ 𝐺 ) ‘ 𝑎 ) ∈ ℕ )
14	5 2 3 13	finodsubmsubg	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )