Theorem cycsubmcmn

Description: The set of nonnegative integer powers of an element A of a monoid forms a commutative monoid. (Contributed by AV, 20-Jan-2024)

	Ref	Expression
Hypotheses	cycsubmcmn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cycsubmcmn.t	⊢ · = ( .g ‘ 𝐺 )
	cycsubmcmn.f	⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
	cycsubmcmn.c	⊢ 𝐶 = ran 𝐹
Assertion	cycsubmcmn	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 𝐺 ↾s 𝐶 ) ∈ CMnd )

Proof

Step	Hyp	Ref	Expression
1		cycsubmcmn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cycsubmcmn.t	⊢ · = ( .g ‘ 𝐺 )
3		cycsubmcmn.f	⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
4		cycsubmcmn.c	⊢ 𝐶 = ran 𝐹
5	1 2 3 4	cycsubm	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ∈ ( SubMnd ‘ 𝐺 ) )
6		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7		eqid	⊢ ( 𝐺 ↾s 𝐶 ) = ( 𝐺 ↾s 𝐶 )
8	1 6 7	issubm2	⊢ ( 𝐺 ∈ Mnd → ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝐶 ⊆ 𝐵 ∧ ( 0g ‘ 𝐺 ) ∈ 𝐶 ∧ ( 𝐺 ↾s 𝐶 ) ∈ Mnd ) ) )
9	8	adantr	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝐶 ⊆ 𝐵 ∧ ( 0g ‘ 𝐺 ) ∈ 𝐶 ∧ ( 𝐺 ↾s 𝐶 ) ∈ Mnd ) ) )
10		simp3	⊢ ( ( 𝐶 ⊆ 𝐵 ∧ ( 0g ‘ 𝐺 ) ∈ 𝐶 ∧ ( 𝐺 ↾s 𝐶 ) ∈ Mnd ) → ( 𝐺 ↾s 𝐶 ) ∈ Mnd )
11	9 10	biimtrdi	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐺 ↾s 𝐶 ) ∈ Mnd ) )
12	5 11	mpd	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 𝐺 ↾s 𝐶 ) ∈ Mnd )
13	7	submbas	⊢ ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) → 𝐶 = ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) )
14	5 13	syl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → 𝐶 = ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) )
15	14	eqcomd	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) = 𝐶 )
16	15	eleq2d	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ↔ 𝑥 ∈ 𝐶 ) )
17	15	eleq2d	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 𝑦 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ↔ 𝑦 ∈ 𝐶 ) )
18	16 17	anbi12d	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) )
19		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
20	1 2 3 4 19	cycsubmcom	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
21	5	adantr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐶 ∈ ( SubMnd ‘ 𝐺 ) )
22	7 19	ressplusg	⊢ ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) )
23	22	eqcomd	⊢ ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) → ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) = ( +g ‘ 𝐺 ) )
24	23	oveqd	⊢ ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑥 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
25	23	oveqd	⊢ ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑦 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑥 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
26	24 25	eqeq12d	⊢ ( 𝐶 ∈ ( SubMnd ‘ 𝐺 ) → ( ( 𝑥 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑦 ) = ( 𝑦 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑥 ) ↔ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
27	21 26	syl	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑥 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑦 ) = ( 𝑦 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑥 ) ↔ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
28	20 27	mpbird	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑦 ) = ( 𝑦 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑥 ) )
29	28	ex	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑦 ) = ( 𝑦 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑥 ) ) )
30	18 29	sylbid	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ) → ( 𝑥 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑦 ) = ( 𝑦 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑥 ) ) )
31	30	ralrimivv	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ( 𝑥 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑦 ) = ( 𝑦 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑥 ) )
32		eqid	⊢ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) = ( Base ‘ ( 𝐺 ↾s 𝐶 ) )
33		eqid	⊢ ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) = ( +g ‘ ( 𝐺 ↾s 𝐶 ) )
34	32 33	iscmn	⊢ ( ( 𝐺 ↾s 𝐶 ) ∈ CMnd ↔ ( ( 𝐺 ↾s 𝐶 ) ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐺 ↾s 𝐶 ) ) ( 𝑥 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑦 ) = ( 𝑦 ( +g ‘ ( 𝐺 ↾s 𝐶 ) ) 𝑥 ) ) )
35	12 31 34	sylanbrc	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 𝐺 ↾s 𝐶 ) ∈ CMnd )