Metamath Proof Explorer

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 ∧ 𝐴 ∈ 𝐵 ) ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )