Theorem gsumconstf

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

	Ref	Expression
Hypotheses	gsumconstf.k	|- F/_ k X
	gsumconstf.b	|- B = ( Base ` G )
	gsumconstf.m	|- .x. = ( .g ` G )
Assertion	gsumconstf	|- ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		gsumconstf.k	|- F/_ k X
2		gsumconstf.b	|- B = ( Base ` G )
3		gsumconstf.m	|- .x. = ( .g ` G )
4		nfcv	|- F/_ l X
5		eqidd	|- ( k = l -> X = X )
6	4 1 5	cbvmpt	|- ( k e. A |-> X ) = ( l e. A |-> X )
7	6	oveq2i	|- ( G gsum ( k e. A |-> X ) ) = ( G gsum ( l e. A |-> X ) )
8	2 3	gsumconst	|- ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( G gsum ( l e. A |-> X ) ) = ( ( # ` A ) .x. X ) )
9	7 8	syl5eq	|- ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )