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 ⊢ φ → A ∈ V
sge0iun.b ⊢ φ ∧ x ∈ A → B ∈ W
sge0iun.x ⊢ X = ⋃ x ∈ A B
sge0iun.f ⊢ φ → F : X ⟶ 0 +∞
sge0iun.dj ⊢ φ → Disj x ∈ A B
Assertion sge0iun ⊢ φ → sum^ ⁡ F = sum^ ⁡ x ∈ A ⟼ sum^ ⁡ F ↾ B

Proof

Step Hyp Ref Expression
1 sge0iun.a ⊢ φ → A ∈ V
2 sge0iun.b ⊢ φ ∧ x ∈ A → B ∈ W
3 sge0iun.x ⊢ X = ⋃ x ∈ A B
4 sge0iun.f ⊢ φ → F : X ⟶ 0 +∞
5 sge0iun.dj ⊢ φ → Disj x ∈ A B
6 4 adantr ⊢ φ ∧ x ∈ A → F : X ⟶ 0 +∞
7 6 3adant3 ⊢ φ ∧ x ∈ A ∧ y ∈ B → F : X ⟶ 0 +∞
8 ssiun2 ⊢ x ∈ A → B ⊆ ⋃ x ∈ A B
9 8 adantl ⊢ φ ∧ x ∈ A → B ⊆ ⋃ x ∈ A B
10 3 eqcomi ⊢ ⋃ x ∈ A B = X
11 9 10 sseqtrdi ⊢ φ ∧ x ∈ A → B ⊆ X
12 11 3adant3 ⊢ φ ∧ x ∈ A ∧ y ∈ B → B ⊆ X
13 simp3 ⊢ φ ∧ x ∈ A ∧ y ∈ B → y ∈ B
14 12 13 sseldd ⊢ φ ∧ x ∈ A ∧ y ∈ B → y ∈ X
15 7 14 ffvelcdmd ⊢ φ ∧ x ∈ A ∧ y ∈ B → F ⁡ y ∈ 0 +∞
16 1 2 5 15 sge0iunmpt ⊢ φ → sum^ ⁡ y ∈ ⋃ x ∈ A B ⟼ F ⁡ y = sum^ ⁡ x ∈ A ⟼ sum^ ⁡ y ∈ B ⟼ F ⁡ y
17 3 feq2i ⊢ F : X ⟶ 0 +∞ ↔ F : ⋃ x ∈ A B ⟶ 0 +∞
18 17 a1i ⊢ φ → F : X ⟶ 0 +∞ ↔ F : ⋃ x ∈ A B ⟶ 0 +∞
19 4 18 mpbid ⊢ φ → F : ⋃ x ∈ A B ⟶ 0 +∞
20 19 feqmptd ⊢ φ → F = y ∈ ⋃ x ∈ A B ⟼ F ⁡ y
21 20 fveq2d ⊢ φ → sum^ ⁡ F = sum^ ⁡ y ∈ ⋃ x ∈ A B ⟼ F ⁡ y
22 6 11 fssresd ⊢ φ ∧ x ∈ A → F ↾ B : B ⟶ 0 +∞
23 22 feqmptd ⊢ φ ∧ x ∈ A → F ↾ B = y ∈ B ⟼ F ↾ B ⁡ y
24 fvres ⊢ y ∈ B → F ↾ B ⁡ y = F ⁡ y
25 24 mpteq2ia ⊢ y ∈ B ⟼ F ↾ B ⁡ y = y ∈ B ⟼ F ⁡ y
26 25 a1i ⊢ φ ∧ x ∈ A → y ∈ B ⟼ F ↾ B ⁡ y = y ∈ B ⟼ F ⁡ y
27 23 26 eqtrd ⊢ φ ∧ x ∈ A → F ↾ B = y ∈ B ⟼ F ⁡ y
28 27 fveq2d ⊢ φ ∧ x ∈ A → sum^ ⁡ F ↾ B = sum^ ⁡ y ∈ B ⟼ F ⁡ y
29 28 mpteq2dva ⊢ φ → x ∈ A ⟼ sum^ ⁡ F ↾ B = x ∈ A ⟼ sum^ ⁡ y ∈ B ⟼ F ⁡ y
30 29 fveq2d ⊢ φ → sum^ ⁡ x ∈ A ⟼ sum^ ⁡ F ↾ B = sum^ ⁡ x ∈ A ⟼ sum^ ⁡ y ∈ B ⟼ F ⁡ y
31 16 21 30 3eqtr4d ⊢ φ → sum^ ⁡ F = sum^ ⁡ x ∈ A ⟼ sum^ ⁡ F ↾ B