Theorem gsumconstf

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

	Ref	Expression
Hypotheses	gsumconstf.k	$$⊢\underset{\_}{Ⅎ}kX$$
	gsumconstf.b	$$⊢B={\mathrm{Base}}_G$$
	gsumconstf.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	gsumconstf	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in \mathrm{Fin}\wedge X\in B\right)\to \underset{k\in A}{{\sum }_G}X=\left|A\right|\underset{\dot{}}{·}X$$

Proof

Step	Hyp	Ref	Expression
1		gsumconstf.k	$$⊢\underset{\_}{Ⅎ}kX$$
2		gsumconstf.b	$$⊢B={\mathrm{Base}}_G$$
3		gsumconstf.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}lX$$
5		eqidd	$$⊢k=l\to X=X$$
6	4 1 5	cbvmpt	$$⊢\left(k\in A⟼X\right)=\left(l\in A⟼X\right)$$
7	6	oveq2i	$$⊢\underset{k\in A}{{\sum }_G}X=\underset{l\in A}{{\sum }_G}X$$
8	2 3	gsumconst	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in \mathrm{Fin}\wedge X\in B\right)\to \underset{l\in A}{{\sum }_G}X=\left|A\right|\underset{\dot{}}{·}X$$
9	7 8	syl5eq	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in \mathrm{Fin}\wedge X\in B\right)\to \underset{k\in A}{{\sum }_G}X=\left|A\right|\underset{\dot{}}{·}X$$