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	⊢ Σ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = Σ 𝑘 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
2	1	fvmpt2i	⊢ ( 𝑘 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = ( I ‘ 𝐵 ) )
3	2	sumeq2i	⊢ Σ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 )
4		fveq2	⊢ ( 𝑗 = 𝑘 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) )
5		nffvmpt1	⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 )
6		nfcv	⊢ Ⅎ 𝑗 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 )
7	4 5 6	cbvsum	⊢ Σ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = Σ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 )
8		sum2id	⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 )
9	3 7 8	3eqtr4i	⊢ Σ 𝑗 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = Σ 𝑘 ∈ 𝐴 𝐵