Metamath Proof Explorer


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