Metamath Proof Explorer

Theorem sge0iun

Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0iun.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
sge0iun.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
sge0iun.x ⊢ 𝑋 = ∪ 𝑥 ∈ 𝐴 𝐵
sge0iun.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
sge0iun.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
Assertion sge0iun ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0iun.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 sge0iun.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
3 sge0iun.x ⊢ 𝑋 = ∪ 𝑥 ∈ 𝐴 𝐵
4 sge0iun.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
5 sge0iun.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
6 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
7 6 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
8 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
10 3 eqcomi ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = 𝑋
11 9 10 sseqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 )
12 11 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐵 ⊆ 𝑋 )
13 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
14 12 13 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝑋 )
15 7 14 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
16 1 2 5 15 sge0iunmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
17 3 feq2i ⊢ ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ↔ 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ( 0 [,] +∞ ) )
18 17 a1i ⊢ ( 𝜑 → ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ↔ 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ( 0 [,] +∞ ) ) )
19 4 18 mpbid ⊢ ( 𝜑 → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ( 0 [,] +∞ ) )
20 19 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) )
21 20 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( Σ^ ‘ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
22 6 11 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
23 22 feqmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ 𝐵 ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) )
24 fvres ⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
25 24 mpteq2ia ⊢ ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) )
26 25 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) )
27 23 26 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ 𝐵 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) )
28 27 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = ( Σ^ ‘ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
29 28 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) )
30 29 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
31 16 21 30 3eqtr4d ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ) )