Theorem sge0fodjrn

Description: Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0fodjrn.k	⊢ Ⅎ 𝑘 𝜑
	sge0fodjrn.n	⊢ Ⅎ 𝑛 𝜑
	sge0fodjrn.bd	⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
	sge0fodjrn.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	sge0fodjrn.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –onto→ 𝐴 )
	sge0fodjrn.dj	⊢ ( 𝜑 → Disj 𝑛 ∈ 𝐶 ( 𝐹 ‘ 𝑛 ) )
	sge0fodjrn.fng	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
	sge0fodjrn.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0fodjrn.b0	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → 𝐵 = 0 )
Assertion	sge0fodjrn	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0fodjrn.k	⊢ Ⅎ 𝑘 𝜑
2		sge0fodjrn.n	⊢ Ⅎ 𝑛 𝜑
3		sge0fodjrn.bd	⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
4		sge0fodjrn.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		sge0fodjrn.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –onto→ 𝐴 )
6		sge0fodjrn.dj	⊢ ( 𝜑 → Disj 𝑛 ∈ 𝐶 ( 𝐹 ‘ 𝑛 ) )
7		sge0fodjrn.fng	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
8		sge0fodjrn.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
9		sge0fodjrn.b0	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → 𝐵 = 0 )
10		eqid	⊢ ( ◡ 𝐹 “ { ∅ } ) = ( ◡ 𝐹 “ { ∅ } )
11	1 2 3 4 5 6 7 8 9 10	sge0fodjrnlem	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) )