sge0less

Description: A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0less.1	$⊢ φ \to X \in V$
	sge0less.2	$⊢ φ \to F : X ⟶ [0, +∞]$
Assertion	sge0less	$⊢ φ \to sum^({F ↾}_{Y}) \leq sum^(F)$

Proof

Step	Hyp	Ref	Expression
1		sge0less.1	$⊢ φ \to X \in V$
2		sge0less.2	$⊢ φ \to F : X ⟶ [0, +∞]$
3		inex1g	$⊢ X \in V \to X \cap Y \in V$
4	1 3	syl	$⊢ φ \to X \cap Y \in V$
5		fresin	$⊢ F : X ⟶ [0, +∞] \to ({F ↾}_{Y}) : X \cap Y ⟶ [0, +∞]$
6	2 5	syl	$⊢ φ \to ({F ↾}_{Y}) : X \cap Y ⟶ [0, +∞]$
7	4 6	sge0xrcl	$⊢ φ \to sum^({F ↾}_{Y}) \in ℝ^{*}$
8		pnfge	$⊢ sum^({F ↾}_{Y}) \in ℝ^{*} \to sum^({F ↾}_{Y}) \leq +∞$
9	7 8	syl	$⊢ φ \to sum^({F ↾}_{Y}) \leq +∞$
10	9	adantr	$⊢ (φ \land sum^(F) = +∞) \to sum^({F ↾}_{Y}) \leq +∞$
11		id	$⊢ sum^(F) = +∞ \to sum^(F) = +∞$
12	11	eqcomd	$⊢ sum^(F) = +∞ \to +∞ = sum^(F)$
13	12	adantl	$⊢ (φ \land sum^(F) = +∞) \to +∞ = sum^(F)$
14	10 13	breqtrd	$⊢ (φ \land sum^(F) = +∞) \to sum^({F ↾}_{Y}) \leq sum^(F)$
15		simpl	$⊢ (φ \land \neg sum^(F) = +∞) \to φ$
16		simpr	$⊢ (φ \land \neg sum^(F) = +∞) \to \neg sum^(F) = +∞$
17	15 1	syl	$⊢ (φ \land \neg sum^(F) = +∞) \to X \in V$
18	15 2	syl	$⊢ (φ \land \neg sum^(F) = +∞) \to F : X ⟶ [0, +∞]$
19	17 18	sge0repnf	$⊢ (φ \land \neg sum^(F) = +∞) \to (sum^(F) \in ℝ \leftrightarrow \neg sum^(F) = +∞)$
20	16 19	mpbird	$⊢ (φ \land \neg sum^(F) = +∞) \to sum^(F) \in ℝ$
21		elinel1	$⊢ x \in (𝒫 (X \cap Y) \cap Fin) \to x \in 𝒫 (X \cap Y)$
22		elpwi	$⊢ x \in 𝒫 (X \cap Y) \to x \subseteq X \cap Y$
23	21 22	syl	$⊢ x \in (𝒫 (X \cap Y) \cap Fin) \to x \subseteq X \cap Y$
24		inss2	$⊢ X \cap Y \subseteq Y$
25	24	a1i	$⊢ x \in (𝒫 (X \cap Y) \cap Fin) \to X \cap Y \subseteq Y$
26	23 25	sstrd	$⊢ x \in (𝒫 (X \cap Y) \cap Fin) \to x \subseteq Y$
27	26	adantr	$⊢ (x \in (𝒫 (X \cap Y) \cap Fin) \land y \in x) \to x \subseteq Y$
28		simpr	$⊢ (x \in (𝒫 (X \cap Y) \cap Fin) \land y \in x) \to y \in x$
29	27 28	sseldd	$⊢ (x \in (𝒫 (X \cap Y) \cap Fin) \land y \in x) \to y \in Y$
30		fvres	$⊢ y \in Y \to ({F ↾}_{Y}) (y) = F (y)$
31	29 30	syl	$⊢ (x \in (𝒫 (X \cap Y) \cap Fin) \land y \in x) \to ({F ↾}_{Y}) (y) = F (y)$
32	31	ralrimiva	$⊢ x \in (𝒫 (X \cap Y) \cap Fin) \to \forall y \in x ({F ↾}_{Y}) (y) = F (y)$
33	32	sumeq2d	$⊢ x \in (𝒫 (X \cap Y) \cap Fin) \to \sum_{y \in x} ({F ↾}_{Y}) (y) = \sum_{y \in x} F (y)$
34	33	mpteq2ia	$⊢ (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) = (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} F (y))$
35		inss1	$⊢ X \cap Y \subseteq X$
36	35	sspwi	$⊢ 𝒫 (X \cap Y) \subseteq 𝒫 X$
37		ssrin	$⊢ 𝒫 (X \cap Y) \subseteq 𝒫 X \to 𝒫 (X \cap Y) \cap Fin \subseteq 𝒫 X \cap Fin$
38	36 37	ax-mp	$⊢ 𝒫 (X \cap Y) \cap Fin \subseteq 𝒫 X \cap Fin$
39		mptss	$⊢ 𝒫 (X \cap Y) \cap Fin \subseteq 𝒫 X \cap Fin \to (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
40	38 39	ax-mp	$⊢ (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
41	34 40	eqsstri	$⊢ (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) \subseteq (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
42		rnss	$⊢ (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) \subseteq (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \to ran (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) \subseteq ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
43	41 42	ax-mp	$⊢ ran (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) \subseteq ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
44	43	a1i	$⊢ (φ \land sum^(F) \in ℝ) \to ran (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) \subseteq ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
45	2	adantr	$⊢ (φ \land sum^(F) \in ℝ) \to F : X ⟶ [0, +∞]$
46	1	adantr	$⊢ (φ \land sum^(F) \in ℝ) \to X \in V$
47		simpr	$⊢ (φ \land sum^(F) \in ℝ) \to sum^(F) \in ℝ$
48	46 45 47	sge0rern	$⊢ (φ \land sum^(F) \in ℝ) \to \neg +∞ \in ran F$
49	45 48	fge0iccico	$⊢ (φ \land sum^(F) \in ℝ) \to F : X ⟶ [0, +∞)$
50	49	sge0rnre	$⊢ (φ \land sum^(F) \in ℝ) \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ$
51		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
52	50 51	sstrdi	$⊢ (φ \land sum^(F) \in ℝ) \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{*}$
53		supxrss	$⊢ (ran (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) \subseteq ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \land ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) \subseteq ℝ^{}) \to sup (ran (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) ℝ^{} <) \leq sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
54	44 52 53	syl2anc	$⊢ (φ \land sum^(F) \in ℝ) \to sup (ran (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) ℝ^{} <) \leq sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <)$
55	46 3	syl	$⊢ (φ \land sum^(F) \in ℝ) \to X \cap Y \in V$
56	45 5	syl	$⊢ (φ \land sum^(F) \in ℝ) \to ({F ↾}_{Y}) : X \cap Y ⟶ [0, +∞]$
57		nelrnres	$⊢ \neg +∞ \in ran F \to \neg +∞ \in ran ({F ↾}_{Y})$
58	48 57	syl	$⊢ (φ \land sum^(F) \in ℝ) \to \neg +∞ \in ran ({F ↾}_{Y})$
59	56 58	fge0iccico	$⊢ (φ \land sum^(F) \in ℝ) \to ({F ↾}_{Y}) : X \cap Y ⟶ [0, +∞)$
60	55 59	sge0reval	$⊢ (φ \land sum^(F) \in ℝ) \to sum^({F ↾}_{Y}) = sup (ran (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) ℝ^{*} <)$
61	46 49	sge0reval	$⊢ (φ \land sum^(F) \in ℝ) \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
62	60 61	breq12d	$⊢ (φ \land sum^(F) \in ℝ) \to (sum^({F ↾}_{Y}) \leq sum^(F) \leftrightarrow sup (ran (x \in (𝒫 (X \cap Y) \cap Fin) ⟼ \sum_{y \in x} ({F ↾}_{Y}) (y)) ℝ^{} <) \leq sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <))$
63	54 62	mpbird	$⊢ (φ \land sum^(F) \in ℝ) \to sum^({F ↾}_{Y}) \leq sum^(F)$
64	15 20 63	syl2anc	$⊢ (φ \land \neg sum^(F) = +∞) \to sum^({F ↾}_{Y}) \leq sum^(F)$
65	14 64	pm2.61dan	$⊢ φ \to sum^({F ↾}_{Y}) \leq sum^(F)$

Metamath Proof Explorer

Theorem sge0less

Proof