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 | ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ) |
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 | ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ) |