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	bilani	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ 𝑐 ∈ 𝐶 ) → ∃ 𝑖 ∈ ℕ0 𝑐 = ( 𝑖 · 𝐴 ) )
8	7	ralrimiva	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ∀ 𝑐 ∈ 𝐶 ∃ 𝑖 ∈ ℕ0 𝑐 = ( 𝑖 · 𝐴 ) )
9		simplll	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
10		simprl	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑚 ∈ ℕ0 )
11		simprr	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑛 ∈ ℕ0 )
12		simpllr	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝐴 ∈ 𝐵 )
13	1 2 5	mulgnn0dir	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
14	9 10 11 12 13	syl13anc	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) ∧ ( 𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
15	14	ralrimivva	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ∀ 𝑚 ∈ ℕ0 ∀ 𝑛 ∈ ℕ0 ( ( 𝑚 + 𝑛 ) · 𝐴 ) = ( ( 𝑚 · 𝐴 ) + ( 𝑛 · 𝐴 ) ) )
16		simprl	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐶 )
17		simprr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → 𝑌 ∈ 𝐶 )
18		nn0sscn	⊢ ℕ0 ⊆ ℂ
19	18	a1i	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ℕ0 ⊆ ℂ )
20	8 15 16 17 19	cyccom	⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )