Theorem cycsubmcom

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

	Ref	Expression
Hypotheses	cycsubmcom.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cycsubmcom.t	⊢ · = ( .g ‘ 𝐺 )
	cycsubmcom.f	⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
	cycsubmcom.c	⊢ 𝐶 = ran 𝐹
	cycsubmcom.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	cycsubmcom	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		cycsubmcom.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cycsubmcom.t	⊢ · = ( .g ‘ 𝐺 )
3		cycsubmcom.f	⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
4		cycsubmcom.c	⊢ 𝐶 = ran 𝐹
5		cycsubmcom.p	⊢ + = ( +g ‘ 𝐺 )
6	1 2 3 4	cycsubmel	⊢ ( 𝑐 ∈ 𝐶 ↔ ∃ 𝑖 ∈ ℕ0 𝑐 = ( 𝑖 · 𝐴 ) )
7	6	biimpi	⊢ ( 𝑐 ∈ 𝐶 → ∃ 𝑖 ∈ ℕ0 𝑐 = ( 𝑖 · 𝐴 ) )
8	7	adantl	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ 𝑐 ∈ 𝐶 ) → ∃ 𝑖 ∈ ℕ0 𝑐 = ( 𝑖 · 𝐴 ) )
9	8	ralrimiva	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ∀ 𝑐 ∈ 𝐶 ∃ 𝑖 ∈ ℕ0 𝑐 = ( 𝑖 · 𝐴 ) )
10		simplll	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
11		simprl	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑚 ∈ ℕ0 )
12		simprr	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑛 ∈ ℕ0 )
13		simpllr	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝐴 ∈ 𝐵 )
14	1 2 5	mulgnn0dir	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
15	10 11 12 13 14	syl13anc	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
16	15	ralrimivva	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ∀ 𝑚 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
17		simprl	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐶 )
18		simprr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑌 ∈ 𝐶 )
19		nn0sscn	⊢ ℕ0 ⊆ ℂ
20	19	a1i	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ℕ0 ⊆ ℂ )
21	9 16 17 18 20	cyccom	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )