cycsubm

Description: The set of nonnegative integer powers of an element A of a monoid forms a submonoid containing A (see cycsubmcl ), called the cyclic monoid generated by the element A . This corresponds to the statement in Lang p. 6. (Contributed by AV, 28-Dec-2023)

	Ref	Expression
Hypotheses	cycsubm.b	$⊢ B = {Base}_{G}$
	cycsubm.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	cycsubm.f	$⊢ F = (x \in ℕ_{0} ⟼ x \underset{˙}{\cdot} A)$
	cycsubm.c	$⊢ C = ran F$
Assertion	cycsubm	$⊢ (G \in Mnd \land A \in B) \to C \in SubMnd (G)$

Proof

Step	Hyp	Ref	Expression
1		cycsubm.b	$⊢ B = {Base}_{G}$
2		cycsubm.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		cycsubm.f	$⊢ F = (x \in ℕ_{0} ⟼ x \underset{˙}{\cdot} A)$
4		cycsubm.c	$⊢ C = ran F$
5	1 2	mulgnn0cl	$⊢ (G \in Mnd \land x \in ℕ_{0} \land A \in B) \to x \underset{˙}{\cdot} A \in B$
6	5	3expa	$⊢ ((G \in Mnd \land x \in ℕ_{0}) \land A \in B) \to x \underset{˙}{\cdot} A \in B$
7	6	an32s	$⊢ ((G \in Mnd \land A \in B) \land x \in ℕ_{0}) \to x \underset{˙}{\cdot} A \in B$
8	7 3	fmptd	$⊢ (G \in Mnd \land A \in B) \to F : ℕ_{0} ⟶ B$
9	8	frnd	$⊢ (G \in Mnd \land A \in B) \to ran F \subseteq B$
10	4 9	eqsstrid	$⊢ (G \in Mnd \land A \in B) \to C \subseteq B$
11		0nn0	$⊢ 0 \in ℕ_{0}$
12	11	a1i	$⊢ (G \in Mnd \land A \in B) \to 0 \in ℕ_{0}$
13		oveq1	$⊢ i = 0 \to i \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A$
14	13	eqeq2d	$⊢ i = 0 \to (0_{G} = i \underset{˙}{\cdot} A \leftrightarrow 0_{G} = 0 \underset{˙}{\cdot} A)$
15	14	adantl	$⊢ ((G \in Mnd \land A \in B) \land i = 0) \to (0_{G} = i \underset{˙}{\cdot} A \leftrightarrow 0_{G} = 0 \underset{˙}{\cdot} A)$
16		eqid	$⊢ 0_{G} = 0_{G}$
17	1 16 2	mulg0	$⊢ A \in B \to 0 \underset{˙}{\cdot} A = 0_{G}$
18	17	adantl	$⊢ (G \in Mnd \land A \in B) \to 0 \underset{˙}{\cdot} A = 0_{G}$
19	18	eqcomd	$⊢ (G \in Mnd \land A \in B) \to 0_{G} = 0 \underset{˙}{\cdot} A$
20	12 15 19	rspcedvd	$⊢ (G \in Mnd \land A \in B) \to \exists i \in ℕ_{0} 0_{G} = i \underset{˙}{\cdot} A$
21	1 2 3 4	cycsubmel	$⊢ 0_{G} \in C \leftrightarrow \exists i \in ℕ_{0} 0_{G} = i \underset{˙}{\cdot} A$
22	20 21	sylibr	$⊢ (G \in Mnd \land A \in B) \to 0_{G} \in C$
23		simplr	$⊢ (((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to i \in ℕ_{0}$
24		simpr	$⊢ (((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to j \in ℕ_{0}$
25	23 24	nn0addcld	$⊢ (((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to i + j \in ℕ_{0}$
26	25	adantr	$⊢ ((((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land (b = j \underset{˙}{\cdot} A \land a = i \underset{˙}{\cdot} A)) \to i + j \in ℕ_{0}$
27		oveq1	$⊢ k = i + j \to k \underset{˙}{\cdot} A = (i + j) \underset{˙}{\cdot} A$
28	27	eqeq2d	$⊢ k = i + j \to (a +_{G} b = k \underset{˙}{\cdot} A \leftrightarrow a +_{G} b = (i + j) \underset{˙}{\cdot} A)$
29	28	adantl	$⊢ (((((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land (b = j \underset{˙}{\cdot} A \land a = i \underset{˙}{\cdot} A)) \land k = i + j) \to (a +_{G} b = k \underset{˙}{\cdot} A \leftrightarrow a +_{G} b = (i + j) \underset{˙}{\cdot} A)$
30		oveq12	$⊢ (a = i \underset{˙}{\cdot} A \land b = j \underset{˙}{\cdot} A) \to a +_{G} b = (i \underset{˙}{\cdot} A) +_{G} (j \underset{˙}{\cdot} A)$
31	30	ancoms	$⊢ (b = j \underset{˙}{\cdot} A \land a = i \underset{˙}{\cdot} A) \to a +_{G} b = (i \underset{˙}{\cdot} A) +_{G} (j \underset{˙}{\cdot} A)$
32		simplll	$⊢ (((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to G \in Mnd$
33		simpllr	$⊢ (((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to A \in B$
34		eqid	$⊢ +_{G} = +_{G}$
35	1 2 34	mulgnn0dir	$⊢ (G \in Mnd \land (i \in ℕ_{0} \land j \in ℕ_{0} \land A \in B)) \to (i + j) \underset{˙}{\cdot} A = (i \underset{˙}{\cdot} A) +_{G} (j \underset{˙}{\cdot} A)$
36	32 23 24 33 35	syl13anc	$⊢ (((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to (i + j) \underset{˙}{\cdot} A = (i \underset{˙}{\cdot} A) +_{G} (j \underset{˙}{\cdot} A)$
37	36	eqcomd	$⊢ (((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to (i \underset{˙}{\cdot} A) +_{G} (j \underset{˙}{\cdot} A) = (i + j) \underset{˙}{\cdot} A$
38	31 37	sylan9eqr	$⊢ ((((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land (b = j \underset{˙}{\cdot} A \land a = i \underset{˙}{\cdot} A)) \to a +_{G} b = (i + j) \underset{˙}{\cdot} A$
39	26 29 38	rspcedvd	$⊢ ((((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \land (b = j \underset{˙}{\cdot} A \land a = i \underset{˙}{\cdot} A)) \to \exists k \in ℕ_{0} a +_{G} b = k \underset{˙}{\cdot} A$
40	39	exp32	$⊢ (((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \land j \in ℕ_{0}) \to (b = j \underset{˙}{\cdot} A \to (a = i \underset{˙}{\cdot} A \to \exists k \in ℕ_{0} a +_{G} b = k \underset{˙}{\cdot} A))$
41	40	rexlimdva	$⊢ ((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \to (\exists j \in ℕ_{0} b = j \underset{˙}{\cdot} A \to (a = i \underset{˙}{\cdot} A \to \exists k \in ℕ_{0} a +_{G} b = k \underset{˙}{\cdot} A))$
42	41	com23	$⊢ ((G \in Mnd \land A \in B) \land i \in ℕ_{0}) \to (a = i \underset{˙}{\cdot} A \to (\exists j \in ℕ_{0} b = j \underset{˙}{\cdot} A \to \exists k \in ℕ_{0} a +_{G} b = k \underset{˙}{\cdot} A))$
43	42	rexlimdva	$⊢ (G \in Mnd \land A \in B) \to (\exists i \in ℕ_{0} a = i \underset{˙}{\cdot} A \to (\exists j \in ℕ_{0} b = j \underset{˙}{\cdot} A \to \exists k \in ℕ_{0} a +_{G} b = k \underset{˙}{\cdot} A))$
44	43	impd	$⊢ (G \in Mnd \land A \in B) \to ((\exists i \in ℕ_{0} a = i \underset{˙}{\cdot} A \land \exists j \in ℕ_{0} b = j \underset{˙}{\cdot} A) \to \exists k \in ℕ_{0} a +_{G} b = k \underset{˙}{\cdot} A)$
45	1 2 3 4	cycsubmel	$⊢ a \in C \leftrightarrow \exists i \in ℕ_{0} a = i \underset{˙}{\cdot} A$
46	1 2 3 4	cycsubmel	$⊢ b \in C \leftrightarrow \exists j \in ℕ_{0} b = j \underset{˙}{\cdot} A$
47	45 46	anbi12i	$⊢ (a \in C \land b \in C) \leftrightarrow (\exists i \in ℕ_{0} a = i \underset{˙}{\cdot} A \land \exists j \in ℕ_{0} b = j \underset{˙}{\cdot} A)$
48	1 2 3 4	cycsubmel	$⊢ a +_{G} b \in C \leftrightarrow \exists k \in ℕ_{0} a +_{G} b = k \underset{˙}{\cdot} A$
49	44 47 48	3imtr4g	$⊢ (G \in Mnd \land A \in B) \to ((a \in C \land b \in C) \to a +_{G} b \in C)$
50	49	ralrimivv	$⊢ (G \in Mnd \land A \in B) \to \forall a \in C \forall b \in C a +_{G} b \in C$
51	1 16 34	issubm	$⊢ G \in Mnd \to (C \in SubMnd (G) \leftrightarrow (C \subseteq B \land 0_{G} \in C \land \forall a \in C \forall b \in C a +_{G} b \in C))$
52	51	adantr	$⊢ (G \in Mnd \land A \in B) \to (C \in SubMnd (G) \leftrightarrow (C \subseteq B \land 0_{G} \in C \land \forall a \in C \forall b \in C a +_{G} b \in C))$
53	10 22 50 52	mpbir3and	$⊢ (G \in Mnd \land A \in B) \to C \in SubMnd (G)$

Metamath Proof Explorer

Theorem cycsubm

Proof