finodsubmsubg

Description: A submonoid whose elements have finite order is a subgroup. (Contributed by SN, 31-Jan-2025)

	Ref	Expression
Hypotheses	finodsubmsubg.o	$⊢ O = od (G)$
	finodsubmsubg.g	$⊢ φ \to G \in Grp$
	finodsubmsubg.s	$⊢ φ \to S \in SubMnd (G)$
	finodsubmsubg.1	$⊢ φ \to \forall a \in S O (a) \in ℕ$
Assertion	finodsubmsubg	$⊢ φ \to S \in SubGrp (G)$

Proof

Step	Hyp	Ref	Expression
1		finodsubmsubg.o	$⊢ O = od (G)$
2		finodsubmsubg.g	$⊢ φ \to G \in Grp$
3		finodsubmsubg.s	$⊢ φ \to S \in SubMnd (G)$
4		finodsubmsubg.1	$⊢ φ \to \forall a \in S O (a) \in ℕ$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6		eqid	$⊢ \cdot_{G} = \cdot_{G}$
7		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
8	2	adantr	$⊢ (φ \land a \in S) \to G \in Grp$
9	5	submss	$⊢ S \in SubMnd (G) \to S \subseteq {Base}_{G}$
10	3 9	syl	$⊢ φ \to S \subseteq {Base}_{G}$
11	10	sselda	$⊢ (φ \land a \in S) \to a \in {Base}_{G}$
12	5 1 6 7 8 11	odm1inv	$⊢ (φ \land a \in S) \to (O (a) - 1) \cdot_{G} a = {inv}_{g} (G) (a)$
13	12	adantr	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to (O (a) - 1) \cdot_{G} a = {inv}_{g} (G) (a)$
14		eqid	$⊢ {Base}_{(G ↾_{𝑠} S)} = {Base}_{(G ↾_{𝑠} S)}$
15		eqid	$⊢ \cdot_{(G ↾_{𝑠} S)} = \cdot_{(G ↾_{𝑠} S)}$
16		eqid	$⊢ G ↾_{𝑠} S = G ↾_{𝑠} S$
17	16	submmnd	$⊢ S \in SubMnd (G) \to G ↾_{𝑠} S \in Mnd$
18	3 17	syl	$⊢ φ \to G ↾_{𝑠} S \in Mnd$
19	18	ad2antrr	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to G ↾_{𝑠} S \in Mnd$
20		nnm1nn0	$⊢ O (a) \in ℕ \to O (a) - 1 \in ℕ_{0}$
21	20	adantl	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to O (a) - 1 \in ℕ_{0}$
22		simplr	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to a \in S$
23	16 5	ressbas2	$⊢ S \subseteq {Base}_{G} \to S = {Base}_{(G ↾_{𝑠} S)}$
24	10 23	syl	$⊢ φ \to S = {Base}_{(G ↾_{𝑠} S)}$
25	24	ad2antrr	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to S = {Base}_{(G ↾_{𝑠} S)}$
26	22 25	eleqtrd	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to a \in {Base}_{(G ↾_{𝑠} S)}$
27	14 15 19 21 26	mulgnn0cld	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to (O (a) - 1) \cdot_{(G ↾_{𝑠} S)} a \in {Base}_{(G ↾_{𝑠} S)}$
28	3	ad2antrr	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to S \in SubMnd (G)$
29	6 16 15	submmulg	$⊢ (S \in SubMnd (G) \land O (a) - 1 \in ℕ_{0} \land a \in S) \to (O (a) - 1) \cdot_{G} a = (O (a) - 1) \cdot_{(G ↾_{𝑠} S)} a$
30	28 21 22 29	syl3anc	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to (O (a) - 1) \cdot_{G} a = (O (a) - 1) \cdot_{(G ↾_{𝑠} S)} a$
31	27 30 25	3eltr4d	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to (O (a) - 1) \cdot_{G} a \in S$
32	13 31	eqeltrrd	$⊢ ((φ \land a \in S) \land O (a) \in ℕ) \to {inv}_{g} (G) (a) \in S$
33	32	ex	$⊢ (φ \land a \in S) \to (O (a) \in ℕ \to {inv}_{g} (G) (a) \in S)$
34	33	ralimdva	$⊢ φ \to (\forall a \in S O (a) \in ℕ \to \forall a \in S {inv}_{g} (G) (a) \in S)$
35	4 34	mpd	$⊢ φ \to \forall a \in S {inv}_{g} (G) (a) \in S$
36	7	issubg3	$⊢ G \in Grp \to (S \in SubGrp (G) \leftrightarrow (S \in SubMnd (G) \land \forall a \in S {inv}_{g} (G) (a) \in S))$
37	2 36	syl	$⊢ φ \to (S \in SubGrp (G) \leftrightarrow (S \in SubMnd (G) \land \forall a \in S {inv}_{g} (G) (a) \in S))$
38	3 35 37	mpbir2and	$⊢ φ \to S \in SubGrp (G)$

Metamath Proof Explorer

Theorem finodsubmsubg

Proof