Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0iunmptlemre Structured version   Visualization version   GIF version

Theorem sge0iunmptlemre 41109
Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0iunmptlemre.a (𝜑𝐴𝑉)
sge0iunmptlemre.b ((𝜑𝑥𝐴) → 𝐵𝑊)
sge0iunmptlemre.dj (𝜑Disj 𝑥𝐴 𝐵)
sge0iunmptlemre.c ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
sge0iunmptlemre.re ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
sge0iunmptlemre.sxr (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ∈ ℝ*)
sge0iunmptlemre.ssxr (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
sge0iunmptlemre.f (𝜑 → (𝑘 𝑥𝐴 𝐵𝐶): 𝑥𝐴 𝐵⟶(0[,]+∞))
sge0iunmptlemre.iue (𝜑 𝑥𝐴 𝐵 ∈ V)
Assertion
Ref Expression
sge0iunmptlemre (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Distinct variable groups:   𝐴,𝑘,𝑥   𝐵,𝑘   𝑥,𝐶   𝑥,𝑊   𝜑,𝑘,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑘)   𝑉(𝑥,𝑘)   𝑊(𝑘)

Proof of Theorem sge0iunmptlemre
Dummy variables 𝑏 𝑝 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sge0iunmptlemre.sxr . 2 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ∈ ℝ*)
2 sge0iunmptlemre.ssxr . 2 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
3 elpwinss 39707 . . . . . . . . . 10 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 𝑥𝐴 𝐵)
43resmptd 5655 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → ((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦) = (𝑘𝑦𝐶))
54fveq2d 6410 . . . . . . . 8 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑘𝑦𝐶)))
65adantl 469 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑘𝑦𝐶)))
7 elinel2 3997 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
87adantl 469 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → 𝑦 ∈ Fin)
93sselda 3796 . . . . . . . . . . 11 ((𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ 𝑘𝑦) → 𝑘 𝑥𝐴 𝐵)
10 eliun 4714 . . . . . . . . . . 11 (𝑘 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑘𝐵)
119, 10sylib 209 . . . . . . . . . 10 ((𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ 𝑘𝑦) → ∃𝑥𝐴 𝑘𝐵)
1211adantll 696 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → ∃𝑥𝐴 𝑘𝐵)
13 nfv 2005 . . . . . . . . . . . 12 𝑥𝜑
14 nfcv 2946 . . . . . . . . . . . . 13 𝑥𝑦
15 nfiu1 4740 . . . . . . . . . . . . . . 15 𝑥 𝑥𝐴 𝐵
1615nfpw 4363 . . . . . . . . . . . . . 14 𝑥𝒫 𝑥𝐴 𝐵
17 nfcv 2946 . . . . . . . . . . . . . 14 𝑥Fin
1816, 17nfin 4015 . . . . . . . . . . . . 13 𝑥(𝒫 𝑥𝐴 𝐵 ∩ Fin)
1914, 18nfel 2959 . . . . . . . . . . . 12 𝑥 𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)
2013, 19nfan 1990 . . . . . . . . . . 11 𝑥(𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
21 nfv 2005 . . . . . . . . . . 11 𝑥 𝑘𝑦
2220, 21nfan 1990 . . . . . . . . . 10 𝑥((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦)
23 nfv 2005 . . . . . . . . . 10 𝑥 𝐶 ∈ (0[,)+∞)
24 simp3 1161 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → 𝑘𝐵)
25 sge0iunmptlemre.c . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
26 eqid 2804 . . . . . . . . . . . . . . . 16 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
2726fvmpt2 6510 . . . . . . . . . . . . . . 15 ((𝑘𝐵𝐶 ∈ (0[,]+∞)) → ((𝑘𝐵𝐶)‘𝑘) = 𝐶)
2824, 25, 27syl2anc 575 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → ((𝑘𝐵𝐶)‘𝑘) = 𝐶)
2928eqcomd 2810 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 = ((𝑘𝐵𝐶)‘𝑘))
30253expa 1140 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
3130, 26fmptd 6604 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
32313adant3 1155 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
33 sge0iunmptlemre.b . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → 𝐵𝑊)
34333adant3 1155 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑘𝐵) → 𝐵𝑊)
35 sge0iunmptlemre.re . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
36353adant3 1155 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐴𝑘𝐵) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
3734, 32, 36sge0rern 41082 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐴𝑘𝐵) → ¬ +∞ ∈ ran (𝑘𝐵𝐶))
3832, 37fge0iccico 41064 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → (𝑘𝐵𝐶):𝐵⟶(0[,)+∞))
3938, 24ffvelrnd 6580 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴𝑘𝐵) → ((𝑘𝐵𝐶)‘𝑘) ∈ (0[,)+∞))
4029, 39eqeltrd 2883 . . . . . . . . . . . 12 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,)+∞))
41403exp 1141 . . . . . . . . . . 11 (𝜑 → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,)+∞))))
4241ad2antrr 708 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,)+∞))))
4322, 23, 42rexlimd 3212 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ (0[,)+∞)))
4412, 43mpd 15 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) ∧ 𝑘𝑦) → 𝐶 ∈ (0[,)+∞))
458, 44sge0fsummpt 41084 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑦𝐶)) = Σ𝑘𝑦 𝐶)
46 sseqin2 4014 . . . . . . . . . . . . . 14 (𝑦 𝑥𝐴 𝐵 ↔ ( 𝑥𝐴 𝐵𝑦) = 𝑦)
4746biimpi 207 . . . . . . . . . . . . 13 (𝑦 𝑥𝐴 𝐵 → ( 𝑥𝐴 𝐵𝑦) = 𝑦)
4847eqcomd 2810 . . . . . . . . . . . 12 (𝑦 𝑥𝐴 𝐵𝑦 = ( 𝑥𝐴 𝐵𝑦))
49 iunin1 4775 . . . . . . . . . . . . 13 𝑥𝐴 (𝐵𝑦) = ( 𝑥𝐴 𝐵𝑦)
5049a1i 11 . . . . . . . . . . . 12 (𝑦 𝑥𝐴 𝐵 𝑥𝐴 (𝐵𝑦) = ( 𝑥𝐴 𝐵𝑦))
5148, 50eqtr4d 2841 . . . . . . . . . . 11 (𝑦 𝑥𝐴 𝐵𝑦 = 𝑥𝐴 (𝐵𝑦))
523, 51syl 17 . . . . . . . . . 10 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → 𝑦 = 𝑥𝐴 (𝐵𝑦))
5352sumeq1d 14652 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) → Σ𝑘𝑦 𝐶 = Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶)
5453adantl 469 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘𝑦 𝐶 = Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶)
55 simpl 470 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → 𝜑)
5633adantlr 697 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑥𝐴) → 𝐵𝑊)
57 sge0iunmptlemre.dj . . . . . . . . . . 11 (𝜑Disj 𝑥𝐴 𝐵)
5857adantr 468 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → Disj 𝑥𝐴 𝐵)
59 rge0ssre 12498 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ ℝ
60 ax-resscn 10276 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
6159, 60sstri 3805 . . . . . . . . . . . 12 (0[,)+∞) ⊆ ℂ
6261, 40sseldi 3794 . . . . . . . . . . 11 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ ℂ)
63623adant1r 1216 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑥𝐴𝑘𝐵) → 𝐶 ∈ ℂ)
64 simpr 473 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → 𝑦 ∈ Fin)
6556, 58, 63, 64fsumiunss 40285 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6655, 8, 65syl2anc 575 . . . . . . . 8 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘 𝑥𝐴 (𝐵𝑦)𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6754, 66eqtrd 2838 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑘𝑦 𝐶 = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
686, 45, 673eqtrd 2842 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
6956, 58, 64disjinfi 39867 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ∈ Fin)
70 id 22 . . . . . . . . . . . . 13 (𝑦 ∈ Fin → 𝑦 ∈ Fin)
71 inss2 4028 . . . . . . . . . . . . . 14 (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦
7271a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ Fin → (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦)
73 ssfi 8417 . . . . . . . . . . . . 13 ((𝑦 ∈ Fin ∧ (𝑤 / 𝑥𝐵𝑦) ⊆ 𝑦) → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
7470, 72, 73syl2anc 575 . . . . . . . . . . . 12 (𝑦 ∈ Fin → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
7574ad2antlr 709 . . . . . . . . . . 11 (((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (𝑤 / 𝑥𝐵𝑦) ∈ Fin)
76 simpll 774 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝜑)
77 elrabi 3552 . . . . . . . . . . . . . 14 (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → 𝑤𝐴)
7877ad2antlr 709 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑤𝐴)
79 elinel1 3996 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) → 𝑘𝑤 / 𝑥𝐵)
8079adantl 469 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑘𝑤 / 𝑥𝐵)
81 nfv 2005 . . . . . . . . . . . . . . . 16 𝑥 𝑤𝐴
82 nfcv 2946 . . . . . . . . . . . . . . . . 17 𝑥𝑘
83 nfcsb1v 3742 . . . . . . . . . . . . . . . . 17 𝑥𝑤 / 𝑥𝐵
8482, 83nfel 2959 . . . . . . . . . . . . . . . 16 𝑥 𝑘𝑤 / 𝑥𝐵
8513, 81, 84nf3an 1993 . . . . . . . . . . . . . . 15 𝑥(𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵)
8685, 23nfim 1987 . . . . . . . . . . . . . 14 𝑥((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))
87 eleq1w 2866 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
88 csbeq1a 3735 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤𝐵 = 𝑤 / 𝑥𝐵)
8988eleq2d 2869 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑘𝐵𝑘𝑤 / 𝑥𝐵))
9087, 893anbi23d 1556 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → ((𝜑𝑥𝐴𝑘𝐵) ↔ (𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵)))
9190imbi1d 332 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,)+∞)) ↔ ((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))))
9286, 91, 40chvar 2436 . . . . . . . . . . . . 13 ((𝜑𝑤𝐴𝑘𝑤 / 𝑥𝐵) → 𝐶 ∈ (0[,)+∞))
9376, 78, 80, 92syl3anc 1483 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
9493adantllr 701 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
9575, 94fsumge0cl 40283 . . . . . . . . . 10 (((𝜑𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶 ∈ (0[,)+∞))
9669, 95sge0fsummpt 41084 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)) = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
97 inss2 4028 . . . . . . . . . . . . . . . . 17 (𝐵𝑦) ⊆ 𝑦
9897a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ Fin → (𝐵𝑦) ⊆ 𝑦)
99 ssfi 8417 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ Fin ∧ (𝐵𝑦) ⊆ 𝑦) → (𝐵𝑦) ∈ Fin)
10070, 98, 99syl2anc 575 . . . . . . . . . . . . . . 15 (𝑦 ∈ Fin → (𝐵𝑦) ∈ Fin)
101100ad2antlr 709 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (𝐵𝑦) ∈ Fin)
102 simpll 774 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝜑)
103 rabid 3302 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↔ (𝑥𝐴 ∧ (𝐵𝑦) ≠ ∅))
104103biimpi 207 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → (𝑥𝐴 ∧ (𝐵𝑦) ≠ ∅))
105104simpld 484 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} → 𝑥𝐴)
106105ad2antlr 709 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝑥𝐴)
107 elinel1 3996 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝐵𝑦) → 𝑘𝐵)
108107adantl 469 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝑘𝐵)
109102, 106, 108, 40syl3anc 1483 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
110109adantllr 701 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
111101, 110sge0fsummpt 41084 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) = Σ𝑘 ∈ (𝐵𝑦)𝐶)
112111mpteq2dva 4936 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ Fin) → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶))
113 nfrab1 3309 . . . . . . . . . . . . . 14 𝑥{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}
114 nfcv 2946 . . . . . . . . . . . . . 14 𝑤{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}
115 nfcv 2946 . . . . . . . . . . . . . 14 𝑤Σ𝑘 ∈ (𝐵𝑦)𝐶
11683, 14nfin 4015 . . . . . . . . . . . . . . 15 𝑥(𝑤 / 𝑥𝐵𝑦)
117 nfcv 2946 . . . . . . . . . . . . . . 15 𝑥𝐶
118116, 117nfsum 14642 . . . . . . . . . . . . . 14 𝑥Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶
11988ineq1d 4010 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝐵𝑦) = (𝑤 / 𝑥𝐵𝑦))
120119sumeq1d 14652 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
121113, 114, 115, 118, 120cbvmptf 4940 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
122121a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ Fin) → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵𝑦)𝐶) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶))
123112, 122eqtr2d 2839 . . . . . . . . . . 11 ((𝜑𝑦 ∈ Fin) → (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶) = (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))))
124123fveq2d 6410 . . . . . . . . . 10 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)) = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
125124eqcomd 2810 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)))
126120, 114, 113, 115, 118cbvsum 14646 . . . . . . . . . 10 Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶
127126a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ Fin) → Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = Σ𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)𝐶)
12896, 125, 1273eqtr4d 2848 . . . . . . . 8 ((𝜑𝑦 ∈ Fin) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
12955, 8, 128syl2anc 575 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶)
130129eqcomd 2810 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → Σ𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵𝑦)𝐶 = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
13168, 130eqtrd 2838 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) = (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
132 sge0iunmptlemre.a . . . . . . . . 9 (𝜑𝐴𝑉)
13377ssriv 3800 . . . . . . . . . 10 {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ⊆ 𝐴
134133a1i 11 . . . . . . . . 9 (𝜑 → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ⊆ 𝐴)
135132, 134ssexd 4998 . . . . . . . 8 (𝜑 → {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ∈ V)
136 vex 3392 . . . . . . . . . . . . 13 𝑦 ∈ V
137136inex2 4993 . . . . . . . . . . . 12 (𝑤 / 𝑥𝐵𝑦) ∈ V
138137a1i 11 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑤 / 𝑥𝐵𝑦) ∈ V)
139 icossicc 12477 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ (0[,]+∞)
140 simpll 774 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝜑)
141 simplr 776 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑤𝐴)
14279adantl 469 . . . . . . . . . . . . . 14 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝑘𝑤 / 𝑥𝐵)
143140, 141, 142, 92syl3anc 1483 . . . . . . . . . . . . 13 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,)+∞))
144139, 143sseldi 3794 . . . . . . . . . . . 12 (((𝜑𝑤𝐴) ∧ 𝑘 ∈ (𝑤 / 𝑥𝐵𝑦)) → 𝐶 ∈ (0[,]+∞))
145 eqid 2804 . . . . . . . . . . . 12 (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)
146144, 145fmptd 6604 . . . . . . . . . . 11 ((𝜑𝑤𝐴) → (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶):(𝑤 / 𝑥𝐵𝑦)⟶(0[,]+∞))
147138, 146sge0cl 41075 . . . . . . . . . 10 ((𝜑𝑤𝐴) → (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
14877, 147sylan2 582 . . . . . . . . 9 ((𝜑𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}) → (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
149 nfcv 2946 . . . . . . . . . 10 𝑤^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))
150 nfcv 2946 . . . . . . . . . . 11 𝑥Σ^
151116, 117nfmpt 4938 . . . . . . . . . . 11 𝑥(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)
152150, 151nffv 6416 . . . . . . . . . 10 𝑥^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))
153119mpteq1d 4930 . . . . . . . . . . 11 (𝑥 = 𝑤 → (𝑘 ∈ (𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))
154153fveq2d 6410 . . . . . . . . . 10 (𝑥 = 𝑤 → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) = (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
155113, 114, 149, 152, 154cbvmptf 4940 . . . . . . . . 9 (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
156148, 155fmptd 6604 . . . . . . . 8 (𝜑 → (𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))):{𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅}⟶(0[,]+∞))
157135, 156sge0xrcl 41079 . . . . . . 7 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
158157adantr 468 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
159 eqid 2804 . . . . . . . . 9 (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))) = (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
160147, 159fmptd 6604 . . . . . . . 8 (𝜑 → (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))):𝐴⟶(0[,]+∞))
161132, 160sge0xrcl 41079 . . . . . . 7 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
162161adantr 468 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ∈ ℝ*)
16355, 2syl 17 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
164155fveq2i 6409 . . . . . . . . 9 ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))))
165164a1i 11 . . . . . . . 8 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
166132, 147, 134sge0lessmpt 41093 . . . . . . . 8 (𝜑 → (Σ^‘(𝑤 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
167165, 166eqbrtrd 4864 . . . . . . 7 (𝜑 → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
168167adantr 468 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))))
169149, 152, 154cbvmpt 4941 . . . . . . . . . . 11 (𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))) = (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))
170169eqcomi 2813 . . . . . . . . . 10 (𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))
171170fveq2i 6409 . . . . . . . . 9 ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶))))
172171a1i 11 . . . . . . . 8 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))))
173136inex2 4993 . . . . . . . . . . 11 (𝐵𝑦) ∈ V
174173a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐵𝑦) ∈ V)
175107, 30sylan2 582 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑘 ∈ (𝐵𝑦)) → 𝐶 ∈ (0[,]+∞))
176 eqid 2804 . . . . . . . . . . 11 (𝑘 ∈ (𝐵𝑦) ↦ 𝐶) = (𝑘 ∈ (𝐵𝑦) ↦ 𝐶)
177175, 176fmptd 6604 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝑘 ∈ (𝐵𝑦) ↦ 𝐶):(𝐵𝑦)⟶(0[,]+∞))
178174, 177sge0cl 41075 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
17933, 31sge0cl 41075 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,]+∞))
180 inss1 4027 . . . . . . . . . . 11 (𝐵𝑦) ⊆ 𝐵
181180a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (𝐵𝑦) ⊆ 𝐵)
18233, 30, 181sge0lessmpt 41093 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)) ≤ (Σ^‘(𝑘𝐵𝐶)))
18313, 132, 178, 179, 182sge0lempt 41104 . . . . . . . 8 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
184172, 183eqbrtrd 4864 . . . . . . 7 (𝜑 → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
185184adantr 468 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑤𝐴 ↦ (Σ^‘(𝑘 ∈ (𝑤 / 𝑥𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
186158, 162, 163, 168, 185xrletrd 12209 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘(𝑥 ∈ {𝑥𝐴 ∣ (𝐵𝑦) ≠ ∅} ↦ (Σ^‘(𝑘 ∈ (𝐵𝑦) ↦ 𝐶)))) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
187131, 186eqbrtrd 4864 . . . 4 ((𝜑𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)) → (Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
188187ralrimiva 3152 . . 3 (𝜑 → ∀𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)(Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
189 sge0iunmptlemre.iue . . . 4 (𝜑 𝑥𝐴 𝐵 ∈ V)
190 sge0iunmptlemre.f . . . 4 (𝜑 → (𝑘 𝑥𝐴 𝐵𝐶): 𝑥𝐴 𝐵⟶(0[,]+∞))
191189, 190, 2sge0lefi 41092 . . 3 (𝜑 → ((Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ↔ ∀𝑦 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)(Σ^‘((𝑘 𝑥𝐴 𝐵𝐶) ↾ 𝑦)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
192188, 191mpbird 248 . 2 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ≤ (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
193 elpwinss 39707 . . . . . . . . 9 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦𝐴)
194193resmptd 5655 . . . . . . . 8 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦) = (𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶))))
195194fveq2d 6410 . . . . . . 7 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
196195adantl 469 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
197 elinel2 3997 . . . . . . . 8 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
198197adantl 469 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
199 0xr 10369 . . . . . . . . 9 0 ∈ ℝ*
200199a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 0 ∈ ℝ*)
201 pnfxr 10375 . . . . . . . . 9 +∞ ∈ ℝ*
202201a1i 11 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → +∞ ∈ ℝ*)
203 simpll 774 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝜑)
204193sselda 3796 . . . . . . . . . . 11 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑥𝑦) → 𝑥𝐴)
205204adantll 696 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝑥𝐴)
206203, 205, 33syl2anc 575 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 𝐵𝑊)
207203, 205, 31syl2anc 575 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
208206, 207sge0xrcl 41079 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ*)
209206, 207sge0ge0 41078 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → 0 ≤ (Σ^‘(𝑘𝐵𝐶)))
210203, 205, 35syl2anc 575 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ ℝ)
211 ltpnf 12168 . . . . . . . . 9 ((Σ^‘(𝑘𝐵𝐶)) ∈ ℝ → (Σ^‘(𝑘𝐵𝐶)) < +∞)
212210, 211syl 17 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) < +∞)
213200, 202, 208, 209, 212elicod 12440 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,)+∞))
214198, 213sge0fsummpt 41084 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) = Σ𝑥𝑦^‘(𝑘𝐵𝐶)))
215196, 214eqtrd 2838 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) = Σ𝑥𝑦^‘(𝑘𝐵𝐶)))
216 nfv 2005 . . . . . 6 𝑘(𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin))
217189adantr 468 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝐴 𝐵 ∈ V)
218190fvmptelrn 6603 . . . . . . 7 ((𝜑𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
219218adantlr 697 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
220198, 210fsumrecl 14686 . . . . . . 7 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ)
221220rexrd 10372 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
222 nfv 2005 . . . . . . . 8 𝑘((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+)
223 iunss1 4722 . . . . . . . . . . . 12 (𝑦𝐴 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
224193, 223syl 17 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
225224adantl 469 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝑦 𝐵 𝑥𝐴 𝐵)
226217, 225ssexd 4998 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥𝑦 𝐵 ∈ V)
227226adantr 468 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → 𝑥𝑦 𝐵 ∈ V)
228 simpll 774 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝜑)
229225sselda 3796 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝑘 𝑥𝐴 𝐵)
230228, 229, 218syl2anc 575 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
231230adantlr 697 . . . . . . . 8 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
232 simpr 473 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → 𝑝 ∈ ℝ+)
233193adantl 469 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦𝐴)
23457adantr 468 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥𝐴 𝐵)
235 disjss1 4816 . . . . . . . . . . . 12 (𝑦𝐴 → (Disj 𝑥𝐴 𝐵Disj 𝑥𝑦 𝐵))
236233, 234, 235sylc 65 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥𝑦 𝐵)
2372033adant3 1155 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝜑)
2382053adant3 1155 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝑥𝐴)
239 simp3 1161 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝑘𝐵)
240237, 238, 239, 25syl3anc 1483 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥𝑦𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
241198, 206, 236, 240, 210sge0iunmptlemfi 41107 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) = (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))))
242214, 220eqeltrd 2883 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑥𝑦 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ)
243241, 242eqeltrd 2883 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
244243adantr 468 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
245222, 227, 231, 232, 244sge0ltfirpmpt 41102 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → ∃𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)(Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
246 nfv 2005 . . . . . . . 8 𝑏((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+)
247 nfre1 3190 . . . . . . . 8 𝑏𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)
248 sspwb 5105 . . . . . . . . . . . . . . . . . 18 ( 𝑥𝑦 𝐵 𝑥𝐴 𝐵 ↔ 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
249248biimpi 207 . . . . . . . . . . . . . . . . 17 ( 𝑥𝑦 𝐵 𝑥𝐴 𝐵 → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
250223, 249syl 17 . . . . . . . . . . . . . . . 16 (𝑦𝐴 → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
251193, 250syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
252251adantr 468 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝒫 𝑥𝑦 𝐵 ⊆ 𝒫 𝑥𝐴 𝐵)
253 elinel1 3996 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 𝑥𝑦 𝐵)
254253adantl 469 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 𝑥𝑦 𝐵)
255252, 254sseldd 3797 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 𝑥𝐴 𝐵)
256 elinel2 3997 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
257256adantl 469 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
258255, 257elind 3995 . . . . . . . . . . . 12 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
259258ad4ant24 754 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
2602593adant3 1155 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → 𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin))
261221ad2antrr 708 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
2622613adant3 1155 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ∈ ℝ*)
263 nfv 2005 . . . . . . . . . . . . . . . 16 𝑘((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin))
264226adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑥𝑦 𝐵 ∈ V)
265230adantlr 697 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) ∧ 𝑘 𝑥𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
266243adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) ∈ ℝ)
267253elpwid 4361 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → 𝑏 𝑥𝑦 𝐵)
268267adantl 469 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑏 𝑥𝑦 𝐵)
269263, 264, 265, 266, 268sge0ssrempt 41099 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ)
270269rexrd 10372 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ*)
271270adantlr 697 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ*)
272 rpxr 12052 . . . . . . . . . . . . . 14 (𝑝 ∈ ℝ+𝑝 ∈ ℝ*)
273272ad2antlr 709 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ*)
274271, 273xaddcld 12347 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ∈ ℝ*)
2752743adant3 1155 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ∈ ℝ*)
276 simp3 1161 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
277241, 214eqtr2d 2839 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
278277adantr 468 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
2792783ad2ant1 1156 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)))
280269adantlr 697 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → (Σ^‘(𝑘𝑏𝐶)) ∈ ℝ)
281 rpre 12051 . . . . . . . . . . . . . . . 16 (𝑝 ∈ ℝ+𝑝 ∈ ℝ)
282281ad2antlr 709 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ)
283 rexadd 12279 . . . . . . . . . . . . . . 15 (((Σ^‘(𝑘𝑏𝐶)) ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
284280, 282, 283syl2anc 575 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
2852843adant3 1155 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) = ((Σ^‘(𝑘𝑏𝐶)) + 𝑝))
286279, 285breq12d 4855 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → (Σ𝑥𝑦^‘(𝑘𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝) ↔ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)))
287276, 286mpbird 248 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
288262, 275, 287xrltled 12197 . . . . . . . . . 10 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
289 rspe 3188 . . . . . . . . . 10 ((𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin) ∧ Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
290260, 288, 289syl2anc 575 . . . . . . . . 9 ((((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) ∧ 𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) ∧ (Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝)) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
2912903exp 1141 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin) → ((Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))))
292246, 247, 291rexlimd 3212 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → (∃𝑏 ∈ (𝒫 𝑥𝑦 𝐵 ∩ Fin)(Σ^‘(𝑘 𝑥𝑦 𝐵𝐶)) < ((Σ^‘(𝑘𝑏𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝)))
293245, 292mpd 15 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ+) → ∃𝑏 ∈ (𝒫 𝑥𝐴 𝐵 ∩ Fin)Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ ((Σ^‘(𝑘𝑏𝐶)) +𝑒 𝑝))
294216, 217, 219, 221, 293sge0gerpmpt 41096 . . . . 5 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥𝑦^‘(𝑘𝐵𝐶)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
295215, 294eqbrtrd 4864 . . . 4 ((𝜑𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
296295ralrimiva 3152 . . 3 (𝜑 → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
297 eqid 2804 . . . . 5 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))
298179, 297fmptd 6604 . . . 4 (𝜑 → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
299132, 298, 1sge0lefi 41092 . . 3 (𝜑 → ((Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^‘((𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) ↾ 𝑦)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶))))
300296, 299mpbird 248 . 2 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
3011, 2, 192, 300xrletrid 12202 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2976  wral 3094  wrex 3095  {crab 3098  Vcvv 3389  csb 3726  cin 3766  wss 3767  c0 4114  𝒫 cpw 4349   ciun 4710  Disj wdisj 4810   class class class wbr 4842  cmpt 4921  cres 5311  wf 6095  cfv 6099  (class class class)co 6872  Fincfn 8190  cc 10217  cr 10218  0cc0 10219   + caddc 10222  +∞cpnf 10354  *cxr 10356   < clt 10357  cle 10358  +crp 12044   +𝑒 cxad 12158  [,)cico 12393  [,]cicc 12394  Σcsu 14637  Σ^csumge0 41056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5094  ax-un 7177  ax-inf2 8783  ax-ac2 9568  ax-cnex 10275  ax-resscn 10276  ax-1cn 10277  ax-icn 10278  ax-addcl 10279  ax-addrcl 10280  ax-mulcl 10281  ax-mulrcl 10282  ax-mulcom 10283  ax-addass 10284  ax-mulass 10285  ax-distr 10286  ax-i2m1 10287  ax-1ne0 10288  ax-1rid 10289  ax-rnegex 10290  ax-rrecex 10291  ax-cnre 10292  ax-pre-lttri 10293  ax-pre-lttrn 10294  ax-pre-ltadd 10295  ax-pre-mulgt0 10296  ax-pre-sup 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-nel 3080  df-ral 3099  df-rex 3100  df-reu 3101  df-rmo 3102  df-rab 3103  df-v 3391  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4115  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-tp 4373  df-op 4375  df-uni 4629  df-int 4668  df-iun 4712  df-disj 4811  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5217  df-eprel 5222  df-po 5230  df-so 5231  df-fr 5268  df-se 5269  df-we 5270  df-xp 5315  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-res 5321  df-ima 5322  df-pred 5891  df-ord 5937  df-on 5938  df-lim 5939  df-suc 5940  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-isom 6108  df-riota 6833  df-ov 6875  df-oprab 6876  df-mpt2 6877  df-om 7294  df-1st 7396  df-2nd 7397  df-wrecs 7640  df-recs 7702  df-rdg 7740  df-1o 7794  df-oadd 7798  df-er 7977  df-map 8092  df-en 8191  df-dom 8192  df-sdom 8193  df-fin 8194  df-sup 8585  df-oi 8652  df-card 9046  df-acn 9049  df-ac 9220  df-pnf 10359  df-mnf 10360  df-xr 10361  df-ltxr 10362  df-le 10363  df-sub 10551  df-neg 10552  df-div 10968  df-nn 11304  df-2 11362  df-3 11363  df-n0 11558  df-z 11642  df-uz 11903  df-rp 12045  df-xadd 12161  df-ico 12397  df-icc 12398  df-fz 12548  df-fzo 12688  df-seq 13023  df-exp 13082  df-hash 13336  df-cj 14060  df-re 14061  df-im 14062  df-sqrt 14196  df-abs 14197  df-clim 14440  df-sum 14638  df-sumge0 41057
This theorem is referenced by:  sge0iunmpt  41112
  Copyright terms: Public domain W3C validator