Metamath Proof Explorer


Theorem sge0ss

Description: Change the index set to a subset in a sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0ss.kph 𝑘 𝜑
sge0ss.b ( 𝜑𝐵𝑉 )
sge0ss.a ( 𝜑𝐴𝐵 )
sge0ss.c ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
sge0ss.c0 ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 = 0 )
Assertion sge0ss ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = ( Σ^ ‘ ( 𝑘𝐵𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 sge0ss.kph 𝑘 𝜑
2 sge0ss.b ( 𝜑𝐵𝑉 )
3 sge0ss.a ( 𝜑𝐴𝐵 )
4 sge0ss.c ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
5 sge0ss.c0 ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 = 0 )
6 ssexg ( ( 𝐴𝐵𝐵𝑉 ) → 𝐴 ∈ V )
7 3 2 6 syl2anc ( 𝜑𝐴 ∈ V )
8 2 difexd ( 𝜑 → ( 𝐵𝐴 ) ∈ V )
9 disjdif ( 𝐴 ∩ ( 𝐵𝐴 ) ) = ∅
10 9 a1i ( 𝜑 → ( 𝐴 ∩ ( 𝐵𝐴 ) ) = ∅ )
11 0e0iccpnf 0 ∈ ( 0 [,] +∞ )
12 11 a1i ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 0 ∈ ( 0 [,] +∞ ) )
13 5 12 eqeltrd ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
14 1 7 8 10 4 13 sge0splitmpt ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵𝐴 ) ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ) ) )
15 14 eqcomd ( 𝜑 → ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵𝐴 ) ) ↦ 𝐶 ) ) )
16 1 5 mpteq2da ( 𝜑 → ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) = ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 0 ) )
17 16 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 0 ) ) )
18 1 8 sge0z ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 0 ) ) = 0 )
19 17 18 eqtrd ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ) = 0 )
20 19 oveq2d ( 𝜑 → ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 0 ) )
21 eqid ( 𝑘𝐴𝐶 ) = ( 𝑘𝐴𝐶 )
22 1 4 21 fmptdf ( 𝜑 → ( 𝑘𝐴𝐶 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
23 7 22 sge0xrcl ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ* )
24 xaddid1 ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) ∈ ℝ* → ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) )
25 23 24 syl ( 𝜑 → ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 0 ) = ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) )
26 eqidd ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) )
27 20 25 26 3eqtrrd ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ) ) )
28 undif ( 𝐴𝐵 ↔ ( 𝐴 ∪ ( 𝐵𝐴 ) ) = 𝐵 )
29 3 28 sylib ( 𝜑 → ( 𝐴 ∪ ( 𝐵𝐴 ) ) = 𝐵 )
30 29 eqcomd ( 𝜑𝐵 = ( 𝐴 ∪ ( 𝐵𝐴 ) ) )
31 30 mpteq1d ( 𝜑 → ( 𝑘𝐵𝐶 ) = ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵𝐴 ) ) ↦ 𝐶 ) )
32 31 fveq2d ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐵𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∪ ( 𝐵𝐴 ) ) ↦ 𝐶 ) ) )
33 15 27 32 3eqtr4d ( 𝜑 → ( Σ^ ‘ ( 𝑘𝐴𝐶 ) ) = ( Σ^ ‘ ( 𝑘𝐵𝐶 ) ) )