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	⊢ Ⅎ 𝑘 𝐴
	esumrnmpt.1	⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
	esumrnmpt.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	esumrnmpt.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
	esumrnmpt.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 𝑊 ∖ { ∅ } ) )
	esumrnmpt.5	⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
Assertion	esumrnmpt	⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		esumrnmpt.0	⊢ Ⅎ 𝑘 𝐴
2		esumrnmpt.1	⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
3		esumrnmpt.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		esumrnmpt.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
5		esumrnmpt.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 𝑊 ∖ { ∅ } ) )
6		esumrnmpt.5	⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
7		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
8	7	rnmpt	⊢ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 }
9		esumeq1	⊢ ( ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑦 ∈ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } 𝐶 )
10	8 9	ax-mp	⊢ Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑦 ∈ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } 𝐶
11		nfcv	⊢ Ⅎ 𝑘 𝐶
12		nfv	⊢ Ⅎ 𝑘 𝜑
13	12 1 5 6	disjdsct	⊢ ( 𝜑 → Fun ◡ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
14	11 12 1 2 3 13 4 5	esumc	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐷 = Σ* 𝑦 ∈ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } 𝐶 )
15	10 14	eqtr4id	⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐷 )