Metamath Proof Explorer

Theorem esumrnmpt

Description: Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 27-May-2020)

Ref Expression
Hypotheses esumrnmpt.0 ⊢ Ⅎ _ k A
esumrnmpt.1 ⊢ y = B → C = D
esumrnmpt.2 ⊢ φ → A ∈ V
esumrnmpt.3 ⊢ φ ∧ k ∈ A → D ∈ 0 +∞
esumrnmpt.4 ⊢ φ ∧ k ∈ A → B ∈ W ∖ ∅
esumrnmpt.5 ⊢ φ → Disj k ∈ A B
Assertion esumrnmpt ⊢ φ → ∑ * y ∈ ran ⁡ k ∈ A ⟼ B C = ∑ * k ∈ A D

Proof

Step Hyp Ref Expression
1 esumrnmpt.0 ⊢ Ⅎ _ k A
2 esumrnmpt.1 ⊢ y = B → C = D
3 esumrnmpt.2 ⊢ φ → A ∈ V
4 esumrnmpt.3 ⊢ φ ∧ k ∈ A → D ∈ 0 +∞
5 esumrnmpt.4 ⊢ φ ∧ k ∈ A → B ∈ W ∖ ∅
6 esumrnmpt.5 ⊢ φ → Disj k ∈ A B
7 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
8 7 rnmpt ⊢ ran ⁡ k ∈ A ⟼ B = z | ∃ k ∈ A z = B
9 esumeq1 ⊢ ran ⁡ k ∈ A ⟼ B = z | ∃ k ∈ A z = B → ∑ * y ∈ ran ⁡ k ∈ A ⟼ B C = ∑ * y ∈ z | ∃ k ∈ A z = B C
10 8 9 ax-mp ⊢ ∑ * y ∈ ran ⁡ k ∈ A ⟼ B C = ∑ * y ∈ z | ∃ k ∈ A z = B C
11 nfcv ⊢ Ⅎ _ k C
12 nfv ⊢ Ⅎ k φ
13 12 1 5 6 disjdsct ⊢ φ → Fun ⁡ k ∈ A ⟼ B -1
14 11 12 1 2 3 13 4 5 esumc ⊢ φ → ∑ * k ∈ A D = ∑ * y ∈ z | ∃ k ∈ A z = B C
15 10 14 eqtr4id ⊢ φ → ∑ * y ∈ ran ⁡ k ∈ A ⟼ B C = ∑ * k ∈ A D