This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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} (k \in A ⟼ B) (j) = \sum_{k \in A} B$

Proof

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