Metamath Proof Explorer

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 )