Metamath Proof Explorer

Theorem sge0lempt

Description: If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0lempt.xph ⊢ Ⅎ x φ
sge0lempt.a ⊢ φ → A ∈ V
sge0lempt.b ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
sge0lempt.c ⊢ φ ∧ x ∈ A → C ∈ 0 +∞
sge0lempt.le ⊢ φ ∧ x ∈ A → B ≤ C
Assertion sge0lempt ⊢ φ → sum^ ⁡ x ∈ A ⟼ B ≤ sum^ ⁡ x ∈ A ⟼ C

Proof

Step Hyp Ref Expression
1 sge0lempt.xph ⊢ Ⅎ x φ
2 sge0lempt.a ⊢ φ → A ∈ V
3 sge0lempt.b ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
4 sge0lempt.c ⊢ φ ∧ x ∈ A → C ∈ 0 +∞
5 sge0lempt.le ⊢ φ ∧ x ∈ A → B ≤ C
6 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
7 1 3 6 fmptdf ⊢ φ → x ∈ A ⟼ B : A ⟶ 0 +∞
8 eqid ⊢ x ∈ A ⟼ C = x ∈ A ⟼ C
9 1 4 8 fmptdf ⊢ φ → x ∈ A ⟼ C : A ⟶ 0 +∞
10 nfv ⊢ Ⅎ x y ∈ A
11 1 10 nfan ⊢ Ⅎ x φ ∧ y ∈ A
12 nfcv ⊢ Ⅎ _ x y
13 12 nfcsb1 ⊢ Ⅎ _ x ⦋ y / x⦌ B
14 nfcv ⊢ Ⅎ _ x ≤
15 12 nfcsb1 ⊢ Ⅎ _ x ⦋ y / x⦌ C
16 13 14 15 nfbr ⊢ Ⅎ x ⦋ y / x⦌ B ≤ ⦋ y / x⦌ C
17 11 16 nfim ⊢ Ⅎ x φ ∧ y ∈ A → ⦋ y / x⦌ B ≤ ⦋ y / x⦌ C
18 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
19 18 anbi2d ⊢ x = y → φ ∧ x ∈ A ↔ φ ∧ y ∈ A
20 csbeq1a ⊢ x = y → B = ⦋ y / x⦌ B
21 csbeq1a ⊢ x = y → C = ⦋ y / x⦌ C
22 20 21 breq12d ⊢ x = y → B ≤ C ↔ ⦋ y / x⦌ B ≤ ⦋ y / x⦌ C
23 19 22 imbi12d ⊢ x = y → φ ∧ x ∈ A → B ≤ C ↔ φ ∧ y ∈ A → ⦋ y / x⦌ B ≤ ⦋ y / x⦌ C
24 17 23 5 chvarfv ⊢ φ ∧ y ∈ A → ⦋ y / x⦌ B ≤ ⦋ y / x⦌ C
25 simpr ⊢ φ ∧ y ∈ A → y ∈ A
26 13 nfel1 ⊢ Ⅎ x ⦋ y / x⦌ B ∈ 0 +∞
27 11 26 nfim ⊢ Ⅎ x φ ∧ y ∈ A → ⦋ y / x⦌ B ∈ 0 +∞
28 20 eleq1d ⊢ x = y → B ∈ 0 +∞ ↔ ⦋ y / x⦌ B ∈ 0 +∞
29 19 28 imbi12d ⊢ x = y → φ ∧ x ∈ A → B ∈ 0 +∞ ↔ φ ∧ y ∈ A → ⦋ y / x⦌ B ∈ 0 +∞
30 27 29 3 chvarfv ⊢ φ ∧ y ∈ A → ⦋ y / x⦌ B ∈ 0 +∞
31 12 13 20 6 fvmptf ⊢ y ∈ A ∧ ⦋ y / x⦌ B ∈ 0 +∞ → x ∈ A ⟼ B ⁡ y = ⦋ y / x⦌ B
32 25 30 31 syl2anc ⊢ φ ∧ y ∈ A → x ∈ A ⟼ B ⁡ y = ⦋ y / x⦌ B
33 nfcv ⊢ Ⅎ _ x 0 +∞
34 15 33 nfel ⊢ Ⅎ x ⦋ y / x⦌ C ∈ 0 +∞
35 11 34 nfim ⊢ Ⅎ x φ ∧ y ∈ A → ⦋ y / x⦌ C ∈ 0 +∞
36 21 eleq1d ⊢ x = y → C ∈ 0 +∞ ↔ ⦋ y / x⦌ C ∈ 0 +∞
37 19 36 imbi12d ⊢ x = y → φ ∧ x ∈ A → C ∈ 0 +∞ ↔ φ ∧ y ∈ A → ⦋ y / x⦌ C ∈ 0 +∞
38 35 37 4 chvarfv ⊢ φ ∧ y ∈ A → ⦋ y / x⦌ C ∈ 0 +∞
39 12 15 21 8 fvmptf ⊢ y ∈ A ∧ ⦋ y / x⦌ C ∈ 0 +∞ → x ∈ A ⟼ C ⁡ y = ⦋ y / x⦌ C
40 25 38 39 syl2anc ⊢ φ ∧ y ∈ A → x ∈ A ⟼ C ⁡ y = ⦋ y / x⦌ C
41 32 40 breq12d ⊢ φ ∧ y ∈ A → x ∈ A ⟼ B ⁡ y ≤ x ∈ A ⟼ C ⁡ y ↔ ⦋ y / x⦌ B ≤ ⦋ y / x⦌ C
42 24 41 mpbird ⊢ φ ∧ y ∈ A → x ∈ A ⟼ B ⁡ y ≤ x ∈ A ⟼ C ⁡ y
43 2 7 9 42 sge0le ⊢ φ → sum^ ⁡ x ∈ A ⟼ B ≤ sum^ ⁡ x ∈ A ⟼ C