Theorem fsumdifsnconst

Description: The sum of constant terms ( k is not free in C ) over an index set excluding a singleton. (Contributed by AV, 7-Jan-2022)

	Ref	Expression
Assertion	fsumdifsnconst	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\wedge C\in ℂ\right)\to \sum _{k\in A\setminus \left\{B\right\}}C=\left(\left|A\right|-1\right)C$$

Proof

Step	Hyp	Ref	Expression
1		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus \left\{B\right\}\in \mathrm{Fin}$$
2	1	anim1i	$$⊢\left(A\in \mathrm{Fin}\wedge C\in ℂ\right)\to \left(A\setminus \left\{B\right\}\in \mathrm{Fin}\wedge C\in ℂ\right)$$
3	2	3adant2	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\wedge C\in ℂ\right)\to \left(A\setminus \left\{B\right\}\in \mathrm{Fin}\wedge C\in ℂ\right)$$
4		fsumconst	$$⊢\left(A\setminus \left\{B\right\}\in \mathrm{Fin}\wedge C\in ℂ\right)\to \sum _{k\in A\setminus \left\{B\right\}}C=\left|A\setminus \left\{B\right\}\right|C$$
5	3 4	syl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\wedge C\in ℂ\right)\to \sum _{k\in A\setminus \left\{B\right\}}C=\left|A\setminus \left\{B\right\}\right|C$$
6		hashdifsn	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\right)\to \left|A\setminus \left\{B\right\}\right|=\left|A\right|-1$$
7	6	3adant3	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\wedge C\in ℂ\right)\to \left|A\setminus \left\{B\right\}\right|=\left|A\right|-1$$
8	7	oveq1d	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\wedge C\in ℂ\right)\to \left|A\setminus \left\{B\right\}\right|C=\left(\left|A\right|-1\right)C$$
9	5 8	eqtrd	$$⊢\left(A\in \mathrm{Fin}\wedge B\in A\wedge C\in ℂ\right)\to \sum _{k\in A\setminus \left\{B\right\}}C=\left(\left|A\right|-1\right)C$$