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	$⊢ φ \to G \in Grp$
	finsubmsubg.s	$⊢ φ \to S \in SubMnd (G)$
	finsubmsubg.1	$⊢ φ \to B \in Fin$
Assertion	finsubmsubg	$⊢ φ \to S \in SubGrp (G)$

Proof

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

Metamath Proof Explorer

Theorem finsubmsubg

Proof