Theorem sumfc

Description: A lemma to facilitate conversions from the function form to the class-variable form of a sum. (Contributed by Mario Carneiro, 12-Aug-2013) (Revised by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Assertion	sumfc	$$⊢\sum _{j\in A}\left(k\in A⟼B\right)\left(j\right)=\sum _{k\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(k\in A⟼B\right)=\left(k\in A⟼B\right)$$
2	1	fvmpt2i	$$⊢k\in A\to \left(k\in A⟼B\right)\left(k\right)=\mathrm{I}\left(B\right)$$
3	2	sumeq2i	$$⊢\sum _{k\in A}\left(k\in A⟼B\right)\left(k\right)=\sum _{k\in A}\mathrm{I}\left(B\right)$$
4		fveq2	$$⊢j=k\to \left(k\in A⟼B\right)\left(j\right)=\left(k\in A⟼B\right)\left(k\right)$$
5		nffvmpt1	$$⊢\underset{\_}{Ⅎ}k\left(k\in A⟼B\right)\left(j\right)$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}j\left(k\in A⟼B\right)\left(k\right)$$
7	4 5 6	cbvsum	$$⊢\sum _{j\in A}\left(k\in A⟼B\right)\left(j\right)=\sum _{k\in A}\left(k\in A⟼B\right)\left(k\right)$$
8		sum2id	$$⊢\sum _{k\in A}B=\sum _{k\in A}\mathrm{I}\left(B\right)$$
9	3 7 8	3eqtr4i	$$⊢\sum _{j\in A}\left(k\in A⟼B\right)\left(j\right)=\sum _{k\in A}B$$