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

Theorem sge0resplit 45207
Description: Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 45210. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0resplit.a (𝜑𝐴𝑉)
sge0resplit.b (𝜑𝐵𝑊)
sge0resplit.u 𝑈 = (𝐴𝐵)
sge0resplit.in0 (𝜑 → (𝐴𝐵) = ∅)
sge0resplit.f (𝜑𝐹:𝑈⟶(0[,]+∞))
sge0resplit.re (𝜑 → (Σ^𝐹) ∈ ℝ)
Assertion
Ref Expression
sge0resplit (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))

Proof of Theorem sge0resplit
Dummy variables 𝑎 𝑏 𝑟 𝑢 𝑣 𝑥 𝑦 𝑡 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sge0resplit.a . . . . . . 7 (𝜑𝐴𝑉)
2 sge0resplit.f . . . . . . . 8 (𝜑𝐹:𝑈⟶(0[,]+∞))
3 ssun1 4172 . . . . . . . . . 10 𝐴 ⊆ (𝐴𝐵)
4 sge0resplit.u . . . . . . . . . . 11 𝑈 = (𝐴𝐵)
54eqcomi 2741 . . . . . . . . . 10 (𝐴𝐵) = 𝑈
63, 5sseqtri 4018 . . . . . . . . 9 𝐴𝑈
76a1i 11 . . . . . . . 8 (𝜑𝐴𝑈)
82, 7fssresd 6758 . . . . . . 7 (𝜑 → (𝐹𝐴):𝐴⟶(0[,]+∞))
94a1i 11 . . . . . . . . 9 (𝜑𝑈 = (𝐴𝐵))
10 sge0resplit.b . . . . . . . . . 10 (𝜑𝐵𝑊)
11 unexg 7738 . . . . . . . . . 10 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
121, 10, 11syl2anc 584 . . . . . . . . 9 (𝜑 → (𝐴𝐵) ∈ V)
139, 12eqeltrd 2833 . . . . . . . 8 (𝜑𝑈 ∈ V)
14 sge0resplit.re . . . . . . . 8 (𝜑 → (Σ^𝐹) ∈ ℝ)
1513, 2, 14sge0ssre 45198 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐴)) ∈ ℝ)
161, 8, 15sge0supre 45190 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ))
1716, 15eqeltrrd 2834 . . . . 5 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) ∈ ℝ)
18 ssun2 4173 . . . . . . . . . 10 𝐵 ⊆ (𝐴𝐵)
1918, 5sseqtri 4018 . . . . . . . . 9 𝐵𝑈
2019a1i 11 . . . . . . . 8 (𝜑𝐵𝑈)
212, 20fssresd 6758 . . . . . . 7 (𝜑 → (𝐹𝐵):𝐵⟶(0[,]+∞))
2213, 2, 14sge0ssre 45198 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐵)) ∈ ℝ)
2310, 21, 22sge0supre 45190 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ))
2423, 22eqeltrrd 2834 . . . . 5 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ) ∈ ℝ)
25 rexadd 13213 . . . . 5 ((sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) ∈ ℝ ∧ sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ) ∈ ℝ) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
2617, 24, 25syl2anc 584 . . . 4 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
2713, 2, 14sge0rern 45189 . . . . . . . 8 (𝜑 → ¬ +∞ ∈ ran 𝐹)
28 nelrnres 43971 . . . . . . . 8 (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹𝐴))
2927, 28syl 17 . . . . . . 7 (𝜑 → ¬ +∞ ∈ ran (𝐹𝐴))
308, 29fge0iccico 45171 . . . . . 6 (𝜑 → (𝐹𝐴):𝐴⟶(0[,)+∞))
3130sge0rnre 45165 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ⊆ ℝ)
32 sge0rnn0 45169 . . . . . 6 ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅
3332a1i 11 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅)
341, 30sge0reval 45173 . . . . . . . 8 (𝜑 → (Σ^‘(𝐹𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ))
3534eqcomd 2738 . . . . . . 7 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) = (Σ^‘(𝐹𝐴)))
3635, 15eqeltrd 2833 . . . . . 6 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ)
37 supxrre3 44120 . . . . . . 7 ((ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤))
3831, 33, 37syl2anc 584 . . . . . 6 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤))
3936, 38mpbid 231 . . . . 5 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤)
40 nelrnres 43971 . . . . . . . 8 (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹𝐵))
4127, 40syl 17 . . . . . . 7 (𝜑 → ¬ +∞ ∈ ran (𝐹𝐵))
4221, 41fge0iccico 45171 . . . . . 6 (𝜑 → (𝐹𝐵):𝐵⟶(0[,)+∞))
4342sge0rnre 45165 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ⊆ ℝ)
44 sge0rnn0 45169 . . . . . 6 ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅
4544a1i 11 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅)
4610, 42sge0reval 45173 . . . . . . . 8 (𝜑 → (Σ^‘(𝐹𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ))
4746eqcomd 2738 . . . . . . 7 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) = (Σ^‘(𝐹𝐵)))
4847, 22eqeltrd 2833 . . . . . 6 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ)
49 supxrre3 44120 . . . . . . 7 ((ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤))
5043, 45, 49syl2anc 584 . . . . . 6 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤))
5148, 50mpbid 231 . . . . 5 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤)
52 eqid 2732 . . . . 5 {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}
5331, 33, 39, 43, 45, 51, 52supadd 12184 . . . 4 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ))
54 simpl 483 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝜑)
55 vex 3478 . . . . . . . . . . . . 13 𝑟 ∈ V
56 eqeq1 2736 . . . . . . . . . . . . . . 15 (𝑧 = 𝑟 → (𝑧 = (𝑣 + 𝑢) ↔ 𝑟 = (𝑣 + 𝑢)))
5756rexbidv 3178 . . . . . . . . . . . . . 14 (𝑧 = 𝑟 → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
5857rexbidv 3178 . . . . . . . . . . . . 13 (𝑧 = 𝑟 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
5955, 58elab 3668 . . . . . . . . . . . 12 (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
6059biimpi 215 . . . . . . . . . . 11 (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
6160adantl 482 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
62 simpl 483 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → 𝜑)
63 vex 3478 . . . . . . . . . . . . . . . . . . . 20 𝑣 ∈ V
64 sumeq1 15637 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎 → Σ𝑦𝑥 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6564cbvmptv 5261 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6665elrnmpt 5955 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦)))
6763, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6867biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6968adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
70 vex 3478 . . . . . . . . . . . . . . . . . . . 20 𝑢 ∈ V
71 sumeq1 15637 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → Σ𝑦𝑥 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7271cbvmptv 5261 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) = (𝑏 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7372elrnmpt 5955 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ V → (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
7470, 73ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7574biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) → ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7675adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7769, 76jca 512 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
78 reeanv 3226 . . . . . . . . . . . . . . . 16 (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) ↔ (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
7977, 78sylibr 233 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
8079adantl 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
81 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
82 elinel1 4195 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ 𝒫 𝐴)
83 elpwi 4609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
84 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎𝐴𝑎𝐴)
8584, 6sstrdi 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎𝐴𝑎𝑈)
8683, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ 𝒫 𝐴𝑎𝑈)
8782, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎𝑈)
8887adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎𝑈)
89 elinel1 4195 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 𝐵)
90 elpwi 4609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ 𝒫 𝐵𝑏𝐵)
91 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏𝐵𝑏𝐵)
9291, 19sstrdi 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏𝐵𝑏𝑈)
9390, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ 𝒫 𝐵𝑏𝑈)
9489, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏𝑈)
9594adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏𝑈)
9688, 95unssd 4186 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ⊆ 𝑈)
97 vex 3478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
98 vex 3478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏 ∈ V
9997, 98unex 7735 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎𝑏) ∈ V
10099elpw 4606 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑏) ∈ 𝒫 𝑈 ↔ (𝑎𝑏) ⊆ 𝑈)
10196, 100sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ 𝒫 𝑈)
102 elinel2 4196 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ Fin)
103102adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ Fin)
104 elinel2 4196 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
105104adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
106 unfi 9174 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ Fin ∧ 𝑏 ∈ Fin) → (𝑎𝑏) ∈ Fin)
107103, 105, 106syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ Fin)
108101, 107elind 4194 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
109108adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
110109ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
111 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → 𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
112 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
113111, 112oveq12d 7429 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑣 + 𝑢) = (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
114113adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
11582, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎𝐴)
116115sselda 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦𝑎) → 𝑦𝐴)
117 fvres 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦𝐴 → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
118116, 117syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦𝑎) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
119118sumeq2dv 15651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 (𝐹𝑦))
120119adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 (𝐹𝑦))
12189, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏𝐵)
122121sselda 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦𝑏) → 𝑦𝐵)
123 fvres 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦𝐵 → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
124122, 123syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦𝑏) → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
125124sumeq2dv 15651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → Σ𝑦𝑏 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 (𝐹𝑦))
126125adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦𝑏 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 (𝐹𝑦))
127120, 126oveq12d 7429 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
128127adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
129114, 128eqtrd 2772 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
130129ad4ant23 751 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑣 + 𝑢) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
131 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = (𝑣 + 𝑢))
132 sge0resplit.in0 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴𝐵) = ∅)
133132adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝐴𝐵) = ∅)
134115ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑎𝐴)
135121adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏𝐵)
136135adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑏𝐵)
137 ssin0 43830 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴𝐵) = ∅ ∧ 𝑎𝐴𝑏𝐵) → (𝑎𝑏) = ∅)
138133, 134, 136, 137syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) = ∅)
139 eqidd 2733 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) = (𝑎𝑏))
140107adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) ∈ Fin)
141 rge0ssre 13435 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
142 ax-resscn 11169 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ⊆ ℂ
143141, 142sstri 3991 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0[,)+∞) ⊆ ℂ
1442, 27fge0iccico 45171 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹:𝑈⟶(0[,)+∞))
145144ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝐹:𝑈⟶(0[,)+∞))
14696sselda 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝑦𝑈)
147146adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝑦𝑈)
148145, 147ffvelcdmd 7087 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → (𝐹𝑦) ∈ (0[,)+∞))
149143, 148sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → (𝐹𝑦) ∈ ℂ)
150138, 139, 140, 149fsumsplit 15689 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
151150ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
152130, 131, 1513eqtr4d 2782 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦))
153 sumeq1 15637 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑎𝑏) → Σ𝑦𝑥 (𝐹𝑦) = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦))
154153rspceeqv 3633 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
155110, 152, 154syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
15655a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ V)
15781, 155, 156elrnmptd 5960 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
158157ex 413 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
159158ex 413 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
160159ex 413 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))))
161160rexlimdvv 3210 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
162161imp 407 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
16362, 80, 162syl2anc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
164163ex 413 . . . . . . . . . . . 12 (𝜑 → ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
165164rexlimdvv 3210 . . . . . . . . . . 11 (𝜑 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
166165imp 407 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
16754, 61, 166syl2anc 584 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
168167ex 413 . . . . . . . 8 (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
16981elrnmpt 5955 . . . . . . . . . . . . 13 (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦)))
170169ibi 266 . . . . . . . . . . . 12 (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
171170adantl 482 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
172 nfv 1917 . . . . . . . . . . . . 13 𝑥𝜑
173 nfcv 2903 . . . . . . . . . . . . . 14 𝑥𝑟
174 nfmpt1 5256 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
175174nfrn 5951 . . . . . . . . . . . . . 14 𝑥ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
176173, 175nfel 2917 . . . . . . . . . . . . 13 𝑥 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
177172, 176nfan 1902 . . . . . . . . . . . 12 𝑥(𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
178 nfmpt1 5256 . . . . . . . . . . . . . 14 𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))
179178nfrn 5951 . . . . . . . . . . . . 13 𝑥ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))
180 nfmpt1 5256 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))
181180nfrn 5951 . . . . . . . . . . . . . 14 𝑥ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))
182 nfv 1917 . . . . . . . . . . . . . 14 𝑥 𝑟 = (𝑣 + 𝑢)
183181, 182nfrexw 3310 . . . . . . . . . . . . 13 𝑥𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
184179, 183nfrexw 3310 . . . . . . . . . . . 12 𝑥𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
185 inss2 4229 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐴) ⊆ 𝐴
186185sseli 3978 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑥𝐴) → 𝑦𝐴)
187186adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥𝐴)) → 𝑦𝐴)
188117eqcomd 2738 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐴 → (𝐹𝑦) = ((𝐹𝐴)‘𝑦))
189187, 188syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥𝐴)) → (𝐹𝑦) = ((𝐹𝐴)‘𝑦))
190189sumeq2dv 15651 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
191 sumeq1 15637 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → Σ𝑦𝑥 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
192191cbvmptv 5261 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
193 vex 3478 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 ∈ V
194193inex1 5317 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐴) ∈ V
195194elpw 4606 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴) ∈ 𝒫 𝐴 ↔ (𝑥𝐴) ⊆ 𝐴)
196185, 195mpbir 230 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐴) ∈ 𝒫 𝐴
197196a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ 𝒫 𝐴)
198 elinel2 4196 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ Fin)
199 inss1 4228 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐴) ⊆ 𝑥
200199a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ⊆ 𝑥)
201 ssfi 9175 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ Fin ∧ (𝑥𝐴) ⊆ 𝑥) → (𝑥𝐴) ∈ Fin)
202198, 200, 201syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ Fin)
203197, 202elind 4194 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ (𝒫 𝐴 ∩ Fin))
204 eqidd 2733 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
205 sumeq1 15637 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑥𝐴) → Σ𝑦𝑧 ((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
206205rspceeqv 3633 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
207203, 204, 206syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
208 sumex 15636 . . . . . . . . . . . . . . . . . . 19 Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ V
209208a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ V)
210192, 207, 209elrnmptd 5960 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
211190, 210eqeltrd 2833 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
2122113ad2ant2 1134 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
213 sumeq1 15637 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → Σ𝑦𝑥 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
214213cbvmptv 5261 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) = (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
215 inss2 4229 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐵) ⊆ 𝐵
216193inex1 5317 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵) ∈ V
217216elpw 4606 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐵) ∈ 𝒫 𝐵 ↔ (𝑥𝐵) ⊆ 𝐵)
218215, 217mpbir 230 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐵) ∈ 𝒫 𝐵
219218a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ 𝒫 𝐵)
220 inss1 4228 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵) ⊆ 𝑥
221220a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ⊆ 𝑥)
222 ssfi 9175 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ Fin ∧ (𝑥𝐵) ⊆ 𝑥) → (𝑥𝐵) ∈ Fin)
223198, 221, 222syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ∈ Fin)
2242233ad2ant2 1134 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ Fin)
225219, 224elind 4194 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ (𝒫 𝐵 ∩ Fin))
226215sseli 3978 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (𝑥𝐵) → 𝑦𝐵)
227123eqcomd 2738 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵 → (𝐹𝑦) = ((𝐹𝐵)‘𝑦))
228226, 227syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝑥𝐵) → (𝐹𝑦) = ((𝐹𝐵)‘𝑦))
229228sumeq2i 15647 . . . . . . . . . . . . . . . . . . . 20 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦)
230229a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
2312303adant3 1132 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
232 sumeq1 15637 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑥𝐵) → Σ𝑦𝑧 ((𝐹𝐵)‘𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
233232rspceeqv 3633 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐵) ∈ (𝒫 𝐵 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
234225, 231, 233syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
235 sumex 15636 . . . . . . . . . . . . . . . . . 18 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ V
236235a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ V)
237214, 234, 236elrnmptd 5960 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))
238 simp3 1138 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 = Σ𝑦𝑥 (𝐹𝑦))
239185a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐴) ⊆ 𝐴)
240215a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵) ⊆ 𝐵)
241 ssin0 43830 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴) ⊆ 𝐴 ∧ (𝑥𝐵) ⊆ 𝐵) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
242132, 239, 240, 241syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
243242adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
244 elinel1 4195 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ 𝒫 𝑈)
245 elpwi 4609 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ 𝒫 𝑈𝑥𝑈)
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥𝑈)
2474ineq2i 4209 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈) = (𝑥 ∩ (𝐴𝐵))
248247a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → (𝑥𝑈) = (𝑥 ∩ (𝐴𝐵)))
249 dfss 3966 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈𝑥 = (𝑥𝑈))
250249biimpi 215 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈𝑥 = (𝑥𝑈))
251 indi 4273 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∩ (𝐴𝐵)) = ((𝑥𝐴) ∪ (𝑥𝐵))
252251eqcomi 2741 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵))
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵)))
254248, 250, 2533eqtr4d 2782 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑈𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
255246, 254syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
256255adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
257198adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 ∈ Fin)
258144ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝐹:𝑈⟶(0[,)+∞))
259246sselda 3982 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑈)
260259adantll 712 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑈)
261258, 260ffvelcdmd 7087 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,)+∞))
262143, 261sselid 3980 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℂ)
263243, 256, 257, 262fsumsplit 15689 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
2642633adant3 1132 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
265238, 264eqtrd 2772 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
266 oveq2 7419 . . . . . . . . . . . . . . . . 17 (𝑢 = Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
267266rspceeqv 3633 . . . . . . . . . . . . . . . 16 ((Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ∧ 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦))) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
268237, 265, 267syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
269 oveq1 7418 . . . . . . . . . . . . . . . . . 18 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (𝑣 + 𝑢) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
270269eqeq2d 2743 . . . . . . . . . . . . . . . . 17 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (𝑟 = (𝑣 + 𝑢) ↔ 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)))
271270rexbidv 3178 . . . . . . . . . . . . . . . 16 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)))
272271rspcev 3612 . . . . . . . . . . . . . . 15 ((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
273212, 268, 272syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
2742733exp 1119 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
275274adantr 481 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
276177, 184, 275rexlimd 3263 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
277171, 276mpd 15 . . . . . . . . . 10 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
278277, 59sylibr 233 . . . . . . . . 9 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)})
279278ex 413 . . . . . . . 8 (𝜑 → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}))
280168, 279impbid 211 . . . . . . 7 (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
281280alrimiv 1930 . . . . . 6 (𝜑 → ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
282 dfcleq 2725 . . . . . 6 ({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
283281, 282sylibr 233 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
284283supeq1d 9443 . . . 4 (𝜑 → sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ))
28526, 53, 2843eqtrrd 2777 . . 3 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
28613, 2, 14sge0supre 45190 . . 3 (𝜑 → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ))
28716, 23oveq12d 7429 . . 3 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
288285, 286, 2873eqtr4d 2782 . 2 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
289 rexadd 13213 . . 3 (((Σ^‘(𝐹𝐴)) ∈ ℝ ∧ (Σ^‘(𝐹𝐵)) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
29015, 22, 289syl2anc 584 . 2 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
291288, 290eqtrd 2772 1 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087  wal 1539   = wceq 1541  wcel 2106  {cab 2709  wne 2940  wral 3061  wrex 3070  Vcvv 3474  cun 3946  cin 3947  wss 3948  c0 4322  𝒫 cpw 4602   class class class wbr 5148  cmpt 5231  ran crn 5677  cres 5678  wf 6539  cfv 6543  (class class class)co 7411  Fincfn 8941  supcsup 9437  cc 11110  cr 11111  0cc0 11112   + caddc 11115  +∞cpnf 11247  *cxr 11249   < clt 11250  cle 11251   +𝑒 cxad 13092  [,)cico 13328  [,]cicc 13329  Σcsu 15634  Σ^csumge0 45163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-xadd 13095  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-seq 13969  df-exp 14030  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-clim 15434  df-sum 15635  df-sumge0 45164
This theorem is referenced by:  sge0split  45210
  Copyright terms: Public domain W3C validator