Theorem gsumconstf

Description: Sum of a constant series. (Contributed by Thierry Arnoux, 5-Jul-2017)

	Ref	Expression
Hypotheses	gsumconstf.k	⊢ Ⅎ 𝑘 𝑋
	gsumconstf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumconstf.m	⊢ · = ( .g ‘ 𝐺 )
Assertion	gsumconstf	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumconstf.k	⊢ Ⅎ 𝑘 𝑋
2		gsumconstf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		gsumconstf.m	⊢ · = ( .g ‘ 𝐺 )
4		nfcv	⊢ Ⅎ 𝑙 𝑋
5		eqidd	⊢ ( 𝑘 = 𝑙 → 𝑋 = 𝑋 )
6	4 1 5	cbvmpt	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑙 ∈ 𝐴 ↦ 𝑋 )
7	6	oveq2i	⊢ ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑙 ∈ 𝐴 ↦ 𝑋 ) )
8	2 3	gsumconst	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑙 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )
9	7 8	eqtrid	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )