Theorem sge0z

Description: Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0z.1	⊢ Ⅎ 𝑘 𝜑
	sge0z.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	sge0z	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		sge0z.1	⊢ Ⅎ 𝑘 𝜑
2		sge0z.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
4	3	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
5	1 4	fmptd2f	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 0 ) : 𝐴 ⟶ ( 0 [,) +∞ ) )
6	2 5	sge0reval	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ‘ 𝑦 ) ) , ℝ* , < ) )
7		eqidd	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑘 ∈ 𝐴 ↦ 0 ) = ( 𝑘 ∈ 𝐴 ↦ 0 ) )
8		eqidd	⊢ ( ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑘 = 𝑦 ) → 0 = 0 )
9		elpwinss	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ⊆ 𝐴 )
10	9	sselda	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐴 )
11		0cnd	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 0 ∈ ℂ )
12	7 8 10 11	fvmptd	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ‘ 𝑦 ) = 0 )
13	12	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ‘ 𝑦 ) = 0 )
14	13	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑥 0 )
15		elinel2	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ Fin )
16		olc	⊢ ( 𝑥 ∈ Fin → ( 𝑥 ⊆ ( ℤ≥ ‘ 𝐵 ) ∨ 𝑥 ∈ Fin ) )
17		sumz	⊢ ( ( 𝑥 ⊆ ( ℤ≥ ‘ 𝐵 ) ∨ 𝑥 ∈ Fin ) → Σ 𝑦 ∈ 𝑥 0 = 0 )
18	15 16 17	3syl	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → Σ 𝑦 ∈ 𝑥 0 = 0 )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 0 = 0 )
20	14 19	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ‘ 𝑦 ) = 0 )
21	20	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) )
22	21	rneqd	⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ‘ 𝑦 ) ) = ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) )
23		eqid	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 )
24		pwfin0	⊢ ( 𝒫 𝐴 ∩ Fin ) ≠ ∅
25	24	a1i	⊢ ( 𝜑 → ( 𝒫 𝐴 ∩ Fin ) ≠ ∅ )
26	23 25	rnmptc	⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = { 0 } )
27	22 26	eqtrd	⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ‘ 𝑦 ) ) = { 0 } )
28	27	supeq1d	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝑘 ∈ 𝐴 ↦ 0 ) ‘ 𝑦 ) ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < ) )
29		xrltso	⊢ < Or ℝ*
30	29	a1i	⊢ ( 𝜑 → < Or ℝ* )
31		0xr	⊢ 0 ∈ ℝ*
32		supsn	⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
33	30 31 32	sylancl	⊢ ( 𝜑 → sup ( { 0 } , ℝ* , < ) = 0 )
34	6 28 33	3eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 )