gsumconstf

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

	Ref	Expression
Hypotheses	gsumconstf.k	$⊢ \underline{Ⅎ} k X$
	gsumconstf.b	$⊢ B = {Base}_{G}$
	gsumconstf.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	gsumconstf	$⊢ (G \in Mnd \land A \in Fin \land X \in B) \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X$

Step	Hyp	Ref	Expression
1		gsumconstf.k	$⊢ \underline{Ⅎ} k X$
2		gsumconstf.b	$⊢ B = {Base}_{G}$
3		gsumconstf.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		nfcv	$⊢ \underline{Ⅎ} l X$
5		eqidd	$⊢ k = l \to X = X$
6	4 1 5	cbvmpt	$⊢ (k \in A ⟼ X) = (l \in A ⟼ X)$
7	6	oveq2i	$⊢ \underset{k \in A}{\sum_{G}} X = \underset{l \in A}{\sum_{G}} X$
8	2 3	gsumconst	$⊢ (G \in Mnd \land A \in Fin \land X \in B) \to \underset{l \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X$
9	7 8	eqtrid	$⊢ (G \in Mnd \land A \in Fin \land X \in B) \to \underset{k \in A}{\sum_{G}} X = \|A\| \underset{˙}{\cdot} X$

Metamath Proof Explorer